aboutsummaryrefslogtreecommitdiff
path: root/lib/system.ml
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2019-11-21 15:38:39 +0100
committerEmilio Jesus Gallego Arias2019-11-21 15:38:39 +0100
commitd016f69818b30b75d186fb14f440b93b0518fc66 (patch)
tree32cd948273f79a2c01ad27b4ed0244ea60d7e2f9 /lib/system.ml
parentb680b06b31c27751a7d551d95839aea38f7fbea1 (diff)
[coq] Untabify the whole ML codebase.
We also remove trailing whitespace. Script used: ```bash for i in `find . -name '*.ml' -or -name '*.mli' -or -name '*.mlg'`; do expand -i "$i" | sponge "$i"; sed -e's/[[:space:]]*$//' -i.bak "$i"; done ```
Diffstat (limited to 'lib/system.ml')
-rw-r--r--lib/system.ml12
1 files changed, 6 insertions, 6 deletions
diff --git a/lib/system.ml b/lib/system.ml
index 8c333ec267..2d68fd2fdf 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -29,9 +29,9 @@ let all_subdirs ~unix_path:root =
let rec traverse path rel =
let f = function
| FileDir (path,f) ->
- let newrel = rel @ [f] in
- add path newrel;
- traverse path newrel
+ let newrel = rel @ [f] in
+ add path newrel;
+ traverse path newrel
| _ -> ()
in process_directory f path
in
@@ -133,7 +133,7 @@ let find_file_in_path ?(warn=true) paths filename =
root, filename
else
CErrors.user_err ~hdr:"System.find_file_in_path"
- (hov 0 (str "Can't find file" ++ spc () ++ str filename))
+ (hov 0 (str "Can't find file" ++ spc () ++ str filename))
else
(* the name is considered to be the transcription as a relative
physical name of a logical name, so we deal with it as a name
@@ -141,8 +141,8 @@ let find_file_in_path ?(warn=true) paths filename =
try where_in_path ~warn paths filename
with Not_found ->
CErrors.user_err ~hdr:"System.find_file_in_path"
- (hov 0 (str "Can't find file" ++ spc () ++ str filename ++ spc () ++
- str "on loadpath"))
+ (hov 0 (str "Can't find file" ++ spc () ++ str filename ++ spc () ++
+ str "on loadpath"))
let is_in_path lpath filename =
try ignore (where_in_path ~warn:false lpath filename); true