[Cmdline] add Filepath parameter
Showing
- src/kernel_internals/runtime/special_hooks.ml 3 additions, 2 deletionssrc/kernel_internals/runtime/special_hooks.ml
- src/kernel_services/cmdline_parameters/parameter_builder.ml 63 additions, 0 deletionssrc/kernel_services/cmdline_parameters/parameter_builder.ml
- src/kernel_services/cmdline_parameters/parameter_customize.ml 4 additions, 0 deletions...kernel_services/cmdline_parameters/parameter_customize.ml
- src/kernel_services/cmdline_parameters/parameter_customize.mli 14 additions, 0 deletions...ernel_services/cmdline_parameters/parameter_customize.mli
- src/kernel_services/cmdline_parameters/parameter_sig.mli 19 additions, 0 deletionssrc/kernel_services/cmdline_parameters/parameter_sig.mli
- src/kernel_services/plugin_entry_points/dynamic.ml 8 additions, 0 deletionssrc/kernel_services/plugin_entry_points/dynamic.ml
- src/kernel_services/plugin_entry_points/dynamic.mli 3 additions, 0 deletionssrc/kernel_services/plugin_entry_points/dynamic.mli
- src/kernel_services/plugin_entry_points/kernel.ml 2 additions, 1 deletionsrc/kernel_services/plugin_entry_points/kernel.ml
- src/kernel_services/plugin_entry_points/kernel.mli 1 addition, 1 deletionsrc/kernel_services/plugin_entry_points/kernel.mli
- src/kernel_services/plugin_entry_points/plugin.ml 1 addition, 1 deletionsrc/kernel_services/plugin_entry_points/plugin.ml
- src/libraries/utils/filepath.ml 2 additions, 0 deletionssrc/libraries/utils/filepath.ml
- src/libraries/utils/filepath.mli 2 additions, 0 deletionssrc/libraries/utils/filepath.mli
- src/plugins/wp/wp_parameters.ml 2 additions, 2 deletionssrc/plugins/wp/wp_parameters.ml
Loading
Please register or sign in to comment