diff options
Diffstat (limited to 'scripts')
| -rw-r--r-- | scripts/coqc.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/scripts/coqc.ml4 b/scripts/coqc.ml4 index a1d64c1d25..c4d6468dd7 100644 --- a/scripts/coqc.ml4 +++ b/scripts/coqc.ml4 @@ -111,7 +111,7 @@ let parse_args () = | "-t" :: rem -> keep := true ; parse (cfiles,args) rem | "-bindir" :: d :: rem -> - bindir := d ; parse (cfiles,d::"-bindir"::args) rem + bindir := d ; parse (cfiles,args) rem | "-bindir" :: [] -> usage () | ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage () |