diff options
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/coqdep_common.ml | 8 | ||||
| -rw-r--r-- | tools/coqmktop.ml | 10 |
2 files changed, 9 insertions, 9 deletions
diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml index 41b026c43d..8c5e5b1ee4 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -265,10 +265,10 @@ let escape = Buffer.clear s'; for i = 0 to String.length s - 1 do let c = s.[i] in - if c = ' ' or c = '#' or c = ':' (* separators and comments *) - or c = '%' (* pattern *) - or c = '?' or c = '[' or c = ']' or c = '*' (* expansion in filenames *) - or i=0 && c = '~' && (String.length s = 1 || s.[1] = '/' || + if c = ' ' || c = '#' || c = ':' (* separators and comments *) + || c = '%' (* pattern *) + || c = '?' || c = '[' || c = ']' || c = '*' (* expansion in filenames *) + || i=0 && c = '~' && (String.length s = 1 || s.[1] = '/' || 'A' <= s.[1] && s.[1] <= 'Z' || 'a' <= s.[1] && s.[1] <= 'z') (* homedir expansion *) then begin diff --git a/tools/coqmktop.ml b/tools/coqmktop.ml index 0ab732da21..0bcd44d0eb 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); |