In the gui and in logs, prints the version and the codename.
Showing
- Makefile.generating 2 additions, 1 deletionMakefile.generating
- src/kernel_internals/runtime/config.ml.in 2 additions, 0 deletionssrc/kernel_internals/runtime/config.ml.in
- src/kernel_internals/runtime/config.mli 9 additions, 1 deletionsrc/kernel_internals/runtime/config.mli
- src/kernel_internals/runtime/special_hooks.ml 2 additions, 2 deletionssrc/kernel_internals/runtime/special_hooks.ml
- src/kernel_services/cmdline_parameters/cmdline.ml 2 additions, 2 deletionssrc/kernel_services/cmdline_parameters/cmdline.ml
- src/plugins/gui/help_manager.ml 1 addition, 1 deletionsrc/plugins/gui/help_manager.ml
- tests/misc/oracle/debug_category.16.res.oracle 1 addition, 1 deletiontests/misc/oracle/debug_category.16.res.oracle
- tests/misc/oracle/log-file.1.res.oracle 1 addition, 1 deletiontests/misc/oracle/log-file.1.res.oracle
- tests/misc/oracle/plugin-log-all.txt 1 addition, 1 deletiontests/misc/oracle/plugin-log-all.txt
Loading
Please register or sign in to comment