[wp] Option to enable local init smoke
Showing
- src/plugins/wp/doc/manual/wp_plugin.tex 3 additions, 1 deletionsrc/plugins/wp/doc/manual/wp_plugin.tex
- src/plugins/wp/tests/wp_plugin/doomed_localinit.i 13 additions, 0 deletionssrc/plugins/wp/tests/wp_plugin/doomed_localinit.i
- src/plugins/wp/tests/wp_plugin/oracle/doomed_localinit.res.oracle 5 additions, 5 deletions...ins/wp/tests/wp_plugin/oracle/doomed_localinit.res.oracle
- src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_localinit.res.oracle 2 additions, 2 deletions...tests/wp_plugin/oracle_qualif/doomed_localinit.res.oracle
- src/plugins/wp/wpReached.ml 5 additions, 1 deletionsrc/plugins/wp/wpReached.ml
- src/plugins/wp/wp_parameters.ml 8 additions, 0 deletionssrc/plugins/wp/wp_parameters.ml
- src/plugins/wp/wp_parameters.mli 2 additions, 1 deletionsrc/plugins/wp/wp_parameters.mli
Loading
Please register or sign in to comment