diff options
| author | herbelin | 2004-09-04 10:35:12 +0000 |
|---|---|---|
| committer | herbelin | 2004-09-04 10:35:12 +0000 |
| commit | f71e6d16d8ccfb6f808457600df7678ec97225f3 (patch) | |
| tree | 19df05019453c408a45a1305fba5c989822a542d | |
| parent | afe62318bacc276a75554cdb3a1567962d83e18c (diff) | |
Correction commit precedent
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6062 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | scripts/coqc.ml | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/scripts/coqc.ml b/scripts/coqc.ml index 43dc71b259..ee7cf9da15 100644 --- a/scripts/coqc.ml +++ b/scripts/coqc.ml @@ -130,9 +130,12 @@ let parse_args () = image := f; parse (cfiles,args) rem | "-image" :: [] -> usage () - | "-libdir" :: _ :: rem -> warning "option -libdir deprecated\n"; parse rem + | "-libdir" :: _ :: rem -> + print_string "Warning: option -libdir deprecated\n"; flush stdout; + parse (cfiles,args) rem | ("-db"|"-debugger") :: rem -> - warning "option -db/-debugger deprecated\n"; parse rem + print_string "Warning: option -db/-debugger deprecated\n";flush stdout; + parse (cfiles,args) rem | ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage () | ("-I"|"-include"|"-outputstate" |