diff options
| author | Guillaume Melquiond | 2014-06-13 16:45:23 +0200 |
|---|---|---|
| committer | Guillaume Melquiond | 2014-06-13 16:45:23 +0200 |
| commit | 5682084d1e8fa6e624c022554c976245f8519852 (patch) | |
| tree | 0f75402df09e855462d681278111e5c750dffdc7 /tools | |
| parent | 8e8b1672843040a8ee1109b2c470477c915d73cc (diff) | |
Remove documentation for the unsupported options -byte and -opt.
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/coqc.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/coqc.ml b/tools/coqc.ml index d7f1bebdf6..0a9ea4e89f 100644 --- a/tools/coqc.ml +++ b/tools/coqc.ml @@ -82,7 +82,7 @@ let parse_args () = | "-image" :: f :: rem -> image := f; parse (cfiles,args) rem | "-image" :: [] -> usage () | "-byte" :: rem -> binary := "coqtop.byte"; parse (cfiles,args) rem - | "-opt" :: rem -> (* now a no-op *) parse (cfiles,args) rem + | "-opt" :: rem -> binary := "coqtop"; parse (cfiles,args) rem (* Obsolete options *) |