summaryrefslogtreecommitdiff
path: root/math/util.ml
diff options
context:
space:
mode:
Diffstat (limited to 'math/util.ml')
-rw-r--r--math/util.ml17
1 files changed, 17 insertions, 0 deletions
diff --git a/math/util.ml b/math/util.ml
new file mode 100644
index 00000000..f0458562
--- /dev/null
+++ b/math/util.ml
@@ -0,0 +1,17 @@
+let mapjoin f l = (List.fold_left (fun a b -> a ^ (f b)) "" l)
+let mapjoine e f = function
+ [] -> ""
+ | h::t -> (List.fold_left (fun a b -> a ^ e ^ (f b)) (f h) t)
+
+exception FileAlreadyExists
+let open_out_unless_exists path =
+ if Sys.file_exists path
+ then raise FileAlreadyExists
+ else open_out path
+
+let run_in_other_directory tmppath cmd =
+ let prevdir = Sys.getcwd () in(
+ Sys.chdir tmppath;
+ let retval = Sys.command cmd in
+ (Sys.chdir prevdir; retval)
+ )