From 0499144ddd71427fe48d873d41e6362ab0744197 Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Thu, 23 Apr 2020 17:11:18 +0200
Subject: [PATCH] [kernel] Some rephrasing in Specific_dir doc.
---
src/kernel_services/cmdline_parameters/parameter_sig.mli | 8 ++++----
1 file changed, 4 insertions(+), 4 deletions(-)
diff --git a/src/kernel_services/cmdline_parameters/parameter_sig.mli b/src/kernel_services/cmdline_parameters/parameter_sig.mli
index 15e512e3278..9ab4f1cca7e 100644
--- a/src/kernel_services/cmdline_parameters/parameter_sig.mli
+++ b/src/kernel_services/cmdline_parameters/parameter_sig.mli
@@ -308,8 +308,8 @@ module type Specific_dir = sig
?mode:[`Normalize_only | `Create_path | `Must_exist ] ->
string ->
Filepath.Normalized.t
- (** [get_dir ?mode p] returns a local-path [p], relative to the plugin
- <specific-dir> directory, to a sub-directory of the plugin <specific-dir>
+ (** [get_dir ?mode p] returns a (local) path [p], i.e. relative to the plugin
+ <specific-dir> directory, of a sub-directory of the plugin <specific-dir>
directory.
@param mode determines how to handle the resulting path:
+ [Normalize_only] just normalizes the resulting path (default).
@@ -320,8 +320,8 @@ module type Specific_dir = sig
?mode:[`Normalize_only | `Create_path | `Must_exist ] ->
string ->
Filepath.Normalized.t
- (** [get_file ?mode p] returns a local-path [p], relative to the plugin
- <specific-dir> directory, to a file in the plugin <specific-dir>
+ (** [get_file ?mode p] returns a (local) path [p], i.e. relative to the
+ plugin <specific-dir> directory, of a file in the plugin <specific-dir>
directory.
@param mode determines how to handle the resulting path:
+ [Normalize_only] just normalizes the resulting path (default).
--
GitLab