diff options
| author | herbelin | 2000-05-05 13:14:15 +0000 |
|---|---|---|
| committer | herbelin | 2000-05-05 13:14:15 +0000 |
| commit | b70bb75b538495ae45eef61689138212d6f9ad93 (patch) | |
| tree | 31756a47b26f7d19184250cdd8c07ec83291a0f3 /scripts | |
| parent | 7c2e5be2338878975195bb7345163913d8d86f0e (diff) | |
Ajoute option -byte
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@420 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'scripts')
| -rw-r--r-- | scripts/coqc.ml4 | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/scripts/coqc.ml4 b/scripts/coqc.ml4 index d0ef0c5ebc..7e70db6b40 100644 --- a/scripts/coqc.ml4 +++ b/scripts/coqc.ml4 @@ -115,6 +115,8 @@ let parse_args () = bindir := d ; parse (cfiles,args) rem | "-bindir" :: [] -> usage () + | "-byte" :: rem -> + binary := "coqtop.byte"; parse (cfiles,args) rem | "-opt" :: rem -> binary := "coqtop.opt"; parse (cfiles,args) rem | ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage () |