From f71e6d16d8ccfb6f808457600df7678ec97225f3 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 4 Sep 2004 10:35:12 +0000
Subject: Correction commit precedent

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6062 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 scripts/coqc.ml | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

(limited to 'scripts')

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"
-- 
cgit v1.2.3