diff options
Diffstat (limited to 'scripts/coqc.ml')
| -rw-r--r-- | scripts/coqc.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/scripts/coqc.ml b/scripts/coqc.ml index 4234216fa..641a3cf6d 100644 --- a/scripts/coqc.ml +++ b/scripts/coqc.ml @@ -108,6 +108,8 @@ let parse_args () = keep := true ; parse (cfiles,args) rem | ("-verbose" | "--verbose") :: rem -> verbose := true ; parse (cfiles,args) rem + | "-translate" :: rem -> + parse (cfiles,"-ftranslate"::args) rem | "-boot" :: rem -> bindir:= Filename.concat Coq_config.coqtop "bin"; parse (cfiles, "-boot"::args) rem |