From e057a2f9c85e7afd8df561c0d89c23d28375e5c9 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Wed, 21 Mar 2001 10:43:09 +0000
Subject: option -verbose a coqc; option -i supprimée

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

(limited to 'scripts')

diff --git a/scripts/coqc.ml b/scripts/coqc.ml
index d807d5d392..0ef69ab086 100644
--- a/scripts/coqc.ml
+++ b/scripts/coqc.ml
@@ -35,9 +35,11 @@ let _ =
     if c <> "" then bindir := c
   with Not_found -> ()
 
-let specification = ref false
+(* coqc options *)
 
+let specification = ref false
 let keep = ref false
+let verbose = ref false
 
 (* Verifies that a string do not contains others caracters than letters, 
    digits, or `_` *)
@@ -84,7 +86,8 @@ let compile command args file =
   let filevo = Filename.concat dirname (modulename ^ ".vo") in
   let oc = open_out tmpfile in
   Printf.fprintf oc "Module %s.\n" modulename;
-  Printf.fprintf oc "Load \"%s\".\n" file;
+  Printf.fprintf oc "Load %s\"%s\".\n" 
+    (if !verbose then "Verbose " else "") file;
   Printf.fprintf oc "Write Module %s \"%s\".\n" modulename filevo;
   flush oc;
   close_out oc;
@@ -122,6 +125,8 @@ let parse_args () =
 	specification := true ; parse (cfiles,args) rem
     | "-t" :: rem -> 
 	keep := true ; parse (cfiles,args) rem
+    | ("-verbose" | "--verbose") :: rem -> 
+	verbose := true ; parse (cfiles,args) rem
     | "-bindir" :: d :: rem ->
 	bindir := d ; parse (cfiles,args) rem
     | "-bindir" :: []       ->
-- 
cgit v1.2.3