[Filepath] add "/" when concatenating paths via Filepath.Normalized.concat
Showing
- src/kernel_services/plugin_entry_points/plugin.ml 3 additions, 3 deletionssrc/kernel_services/plugin_entry_points/plugin.ml
- src/libraries/utils/filepath.ml 1 addition, 1 deletionsrc/libraries/utils/filepath.ml
- src/libraries/utils/filepath.mli 6 additions, 2 deletionssrc/libraries/utils/filepath.mli
- src/plugins/wp/wp_parameters.ml 3 additions, 3 deletionssrc/plugins/wp/wp_parameters.ml
Loading
Please register or sign in to comment