diff options
Diffstat (limited to 'scripts')
| -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" |