[kernel] we do not expect user dirs to exist
Showing
- src/kernel_services/cmdline_parameters/parameter_sig.ml 21 additions, 2 deletionssrc/kernel_services/cmdline_parameters/parameter_sig.ml
- src/kernel_services/plugin_entry_points/plugin.ml 30 additions, 33 deletionssrc/kernel_services/plugin_entry_points/plugin.ml
- src/kernel_services/plugin_entry_points/plugin.mli 5 additions, 4 deletionssrc/kernel_services/plugin_entry_points/plugin.mli
- src/plugins/gui/gui_parameters.mli 1 addition, 1 deletionsrc/plugins/gui/gui_parameters.mli
Loading
Please register or sign in to comment