aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coqmktop.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tools/coqmktop.ml')
-rw-r--r--tools/coqmktop.ml10
1 files changed, 5 insertions, 5 deletions
diff --git a/tools/coqmktop.ml b/tools/coqmktop.ml
index 0ab732da2..0bcd44d0e 100644
--- a/tools/coqmktop.ml
+++ b/tools/coqmktop.ml
@@ -190,11 +190,11 @@ let parse_args () =
| ("-no-start") :: rem -> no_start:=true; parse (op, fl) rem
| f :: rem ->
if Filename.check_suffix f ".ml"
- or Filename.check_suffix f ".cmx"
- or Filename.check_suffix f ".cmo"
- or Filename.check_suffix f ".cmxa"
- or Filename.check_suffix f ".cma"
- or Filename.check_suffix f ".c" then
+ || Filename.check_suffix f ".cmx"
+ || Filename.check_suffix f ".cmo"
+ || Filename.check_suffix f ".cmxa"
+ || Filename.check_suffix f ".cma"
+ || Filename.check_suffix f ".c" then
parse (op,f::fl) rem
else begin
prerr_endline ("Don't know what to do with " ^ f);