diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-11-30 14:41:00 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-11-30 14:41:00 +0000 |
| commit | f35a9a60f882304ebf49c87ced23a0a0959f44ab (patch) | |
| tree | ef2d99a21ebdf877f6d1b0bb4a99bde4ac28ee96 /scripts/coqc.ml | |
| parent | 0fffe8d30f909612d73b5e927608d881f21423b2 (diff) | |
Changement de la syntaxe des options -I et -R
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1038 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'scripts/coqc.ml')
| -rw-r--r-- | scripts/coqc.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/scripts/coqc.ml b/scripts/coqc.ml index adc521232..ee77b8edb 100644 --- a/scripts/coqc.ml +++ b/scripts/coqc.ml @@ -123,9 +123,10 @@ let parse_args () = | "-opt" :: rem -> binary := "coqtop.opt"; parse (cfiles,args) rem | ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage () - | ("-image"|"-libdir"|"-I"|"-R"|"-include"|"-outputstate"|"-inputstate" - |"-is"|"-load-vernac-source"|"-load-vernac-object"|"-load-ml-source" - |"-require"|"-load-ml-object"|"-user"|"-init-file" as o) :: rem -> + | ("-image"|"-libdir"|"-I"|"-R"|"-as"|"-include"|"-outputstate" + |"-inputstate"|"-is"|"-load-vernac-source"|"-load-vernac-object" + |"-load-ml-source"|"-require"|"-load-ml-object"|"-user" + |"-init-file" as o) :: rem -> begin match rem with | s :: rem' -> parse (cfiles,s::o::args) rem' |