diff options
Diffstat (limited to 'toplevel/coqargs.ml')
| -rw-r--r-- | toplevel/coqargs.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index 6c4ea9afa1..0a32879764 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -176,7 +176,7 @@ let set_batch_mode opts = let add_compile opts verbose s = let opts = set_batch_mode opts in if not opts.glob_opt then Dumpglob.dump_to_dotglob (); - (** make the file name explicit; needed not to break up Coq loadpath stuff. *) + (* make the file name explicit; needed not to break up Coq loadpath stuff. *) let s = let open Filename in if is_implicit s |