aboutsummaryrefslogtreecommitdiffhomepage
path: root/scripts
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2005-11-04 09:05:55 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2005-11-04 09:05:55 +0000
commite79bfe9eddf4e40013d00da21933aaab560cca62 (patch)
treef41caf37ea0604399d23ef03ab3ec725ed54aa51 /scripts
parent3f4bc40ac28dfc6cb205db199daaa4e87d260a99 (diff)
Passage option -w à ocaml
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7513 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'scripts')
-rw-r--r--scripts/coqmktop.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml
index ea807936a..3808cbe10 100644
--- a/scripts/coqmktop.ml
+++ b/scripts/coqmktop.ml
@@ -156,7 +156,7 @@ let parse_args () =
coqide := true; parse (op,fl) rem
| "-v8" :: rem -> parse (op,fl) rem
| "-echo" :: rem -> echo := true ; parse (op,fl) rem
- | ("-cclib"|"-ccopt"|"-I"|"-o" as o) :: rem' ->
+ | ("-cclib"|"-ccopt"|"-I"|"-o"|"-w" as o) :: rem' ->
begin
match rem' with
| a :: rem -> parse (a::o::op,fl) rem