diff options
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 () |