[wp] renamed (old) region annotations
Showing
- src/plugins/wp/RegionAnnot.ml 2 additions, 2 deletionssrc/plugins/wp/RegionAnnot.ml
- src/plugins/wp/tests/wp_region/annot.i 4 additions, 4 deletionssrc/plugins/wp/tests/wp_region/annot.i
- src/plugins/wp/tests/wp_region/annot/a.i 4 additions, 6 deletionssrc/plugins/wp/tests/wp_region/annot/a.i
- src/plugins/wp/tests/wp_region/annot/b.i 4 additions, 6 deletionssrc/plugins/wp/tests/wp_region/annot/b.i
- src/plugins/wp/tests/wp_region/array1.i 1 addition, 1 deletionsrc/plugins/wp/tests/wp_region/array1.i
- src/plugins/wp/tests/wp_region/array2.i 1 addition, 1 deletionsrc/plugins/wp/tests/wp_region/array2.i
- src/plugins/wp/tests/wp_region/fb_ADD.i 1 addition, 1 deletionsrc/plugins/wp/tests/wp_region/fb_ADD.i
- src/plugins/wp/tests/wp_region/fb_SORT.i 4 additions, 4 deletionssrc/plugins/wp/tests/wp_region/fb_SORT.i
- src/plugins/wp/tests/wp_region/oracle/annot.res.oracle 4 additions, 4 deletionssrc/plugins/wp/tests/wp_region/oracle/annot.res.oracle
- src/plugins/wp/tests/wp_region/structarray1.i 1 addition, 1 deletionsrc/plugins/wp/tests/wp_region/structarray1.i
Loading
Please register or sign in to comment