[WP] automatically filter properties with name ‘no_wp:’
Showing
- src/plugins/wp/Changelog 2 additions, 1 deletionsrc/plugins/wp/Changelog
- src/plugins/wp/doc/manual/wp_plugin.tex 3 additions, 0 deletionssrc/plugins/wp/doc/manual/wp_plugin.tex
- src/plugins/wp/tests/wp_plugin/nowp.c 7 additions, 0 deletionssrc/plugins/wp/tests/wp_plugin/nowp.c
- src/plugins/wp/tests/wp_plugin/nowp.c.0.report.json 1 addition, 0 deletionssrc/plugins/wp/tests/wp_plugin/nowp.c.0.report.json
- src/plugins/wp/tests/wp_plugin/oracle/nowp.res.oracle 6 additions, 0 deletionssrc/plugins/wp/tests/wp_plugin/oracle/nowp.res.oracle
- src/plugins/wp/tests/wp_plugin/oracle_qualif/nowp.res.oracle 9 additions, 0 deletionssrc/plugins/wp/tests/wp_plugin/oracle_qualif/nowp.res.oracle
- src/plugins/wp/wpAnnot.ml 1 addition, 1 deletionsrc/plugins/wp/wpAnnot.ml
- src/plugins/wp/wpPropId.ml 30 additions, 21 deletionssrc/plugins/wp/wpPropId.ml
- src/plugins/wp/wpPropId.mli 5 additions, 1 deletionsrc/plugins/wp/wpPropId.mli
Loading
Please register or sign in to comment