diff options
| author | herbelin | 2000-12-06 11:36:16 +0000 |
|---|---|---|
| committer | herbelin | 2000-12-06 11:36:16 +0000 |
| commit | c72588e26c59037fe9a9455f9796c0dfd5bc9ed1 (patch) | |
| tree | 022e41a03cf8d6da62b1cedd0913f8a5339605dc /scripts | |
| parent | 78a213bfd65176dae8418bffb4fd95ef22326c81 (diff) | |
Suppresion de l'option -as, c'est maintenant -R qui devient l'option standard pour associer un nom physique à un nom logique
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1066 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'scripts')
| -rw-r--r-- | scripts/coqc.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/scripts/coqc.ml b/scripts/coqc.ml index ee77b8edbd..4dc09bc185 100644 --- a/scripts/coqc.ml +++ b/scripts/coqc.ml @@ -123,7 +123,7 @@ let parse_args () = | "-opt" :: rem -> binary := "coqtop.opt"; parse (cfiles,args) rem | ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage () - | ("-image"|"-libdir"|"-I"|"-R"|"-as"|"-include"|"-outputstate" + | ("-image"|"-libdir"|"-I"|"-include"|"-outputstate" |"-inputstate"|"-is"|"-load-vernac-source"|"-load-vernac-object" |"-load-ml-source"|"-require"|"-load-ml-object"|"-user" |"-init-file" as o) :: rem -> @@ -132,6 +132,7 @@ let parse_args () = | s :: rem' -> parse (cfiles,s::o::args) rem' | [] -> usage () end + | "-R" as o :: s :: t :: rem -> parse (cfiles,t::s::o::args) rem | ("-notactics"|"-debug"|"-db"|"-debugger"|"-nolib"|"-batch"|"-nois" |"-q"|"-full"|"-profile"|"-just-parsing"|"-echo" |"-unsafe"|"-quiet" |"-silent" as o) :: rem -> |