diff options
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/coqide.ml | 2 | ||||
| -rw-r--r-- | ide/utils/config_file.mli | 4 | ||||
| -rw-r--r-- | ide/utils/configwin_ihm.ml | 2 |
3 files changed, 4 insertions, 4 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml index b0d90f2cb..ba20c771a 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -1377,7 +1377,7 @@ let check_for_geoproof_input () = full name, with the last occurrence of "coqide" replaced by "coqtop". This should correctly handle the ".opt", ".byte", ".exe" situations. If the replacement fails, we default to "coqtop", hoping it's somewhere - in the path. Note that the -coqtop option to coqide allows to override + in the path. Note that the -coqtop option to coqide overrides this default coqtop path *) let read_coqide_args argv = diff --git a/ide/utils/config_file.mli b/ide/utils/config_file.mli index b9c776828..22328e7f1 100644 --- a/ide/utils/config_file.mli +++ b/ide/utils/config_file.mli @@ -141,8 +141,8 @@ exception Missing_cp of groupable_cp or used to generate command line arguments. The basic usage is to have only one group and one configuration file, -but this mechanism allows to have more, -for instance to have another smaller group for the options to pass on the command line. +but this mechanism allows having more, +for instance having another smaller group for the options to pass on the command line. *) class group : object (** Adds a cp to the group. diff --git a/ide/utils/configwin_ihm.ml b/ide/utils/configwin_ihm.ml index ad12ad5fd..c1062a9db 100644 --- a/ide/utils/configwin_ihm.ml +++ b/ide/utils/configwin_ihm.ml @@ -67,7 +67,7 @@ let html_config_file_and_option () = let last_dir = ref "";; (** This function allows the user to select a file and returns the - selected file name. An optional function allows to change the + selected file name. An optional function allows changing the behaviour of the ok button. A VOIR : mutli-selection ? *) let select_files ?dir |