[kernel] add user directories
Showing
- configurator.ml 24 additions, 1 deletionconfigurator.ml
- src/kernel_internals/runtime/macos_dirs.ml 17 additions, 0 deletionssrc/kernel_internals/runtime/macos_dirs.ml
- src/kernel_internals/runtime/system_config.ml.in 4 additions, 0 deletionssrc/kernel_internals/runtime/system_config.ml.in
- src/kernel_internals/runtime/system_config.mli 12 additions, 0 deletionssrc/kernel_internals/runtime/system_config.mli
- src/kernel_internals/runtime/unix_dirs.ml 20 additions, 0 deletionssrc/kernel_internals/runtime/unix_dirs.ml
- src/kernel_internals/runtime/win_dirs.ml 13 additions, 0 deletionssrc/kernel_internals/runtime/win_dirs.ml
- src/kernel_services/plugin_entry_points/kernel.ml 31 additions, 1 deletionsrc/kernel_services/plugin_entry_points/kernel.ml
- src/kernel_services/plugin_entry_points/kernel.mli 10 additions, 0 deletionssrc/kernel_services/plugin_entry_points/kernel.mli
- src/kernel_services/plugin_entry_points/plugin.ml 65 additions, 28 deletionssrc/kernel_services/plugin_entry_points/plugin.ml
- src/kernel_services/plugin_entry_points/plugin.mli 31 additions, 3 deletionssrc/kernel_services/plugin_entry_points/plugin.mli
- src/plugins/gui/gtk_helper.ml 1 addition, 1 deletionsrc/plugins/gui/gtk_helper.ml
- src/plugins/gui/gui_parameters.ml 2 additions, 0 deletionssrc/plugins/gui/gui_parameters.ml
- src/plugins/gui/gui_parameters.mli 2 additions, 0 deletionssrc/plugins/gui/gui_parameters.mli
Loading
Please register or sign in to comment