summaryrefslogtreecommitdiff
path: root/src/util.ml
diff options
context:
space:
mode:
authorRobert Norton2018-11-19 15:27:24 +0000
committerRobert Norton2018-11-19 15:27:24 +0000
commitb891846bef840ecbe5673c3b22cbd0f2cfceef0f (patch)
treef40a1626b17a3cb0e373aaca925b32c938f52220 /src/util.ml
parent1bc81fa6dcafcfe24fce3685c2eb61f882e6b65c (diff)
parent8c2739ace6ddc9b506d8e6782a4075574115cb34 (diff)
Merge branch 'latex' into sail2
Diffstat (limited to 'src/util.ml')
-rw-r--r--src/util.ml8
1 files changed, 8 insertions, 0 deletions
diff --git a/src/util.ml b/src/util.ml
index 2e121a4f..5e5654d1 100644
--- a/src/util.ml
+++ b/src/util.ml
@@ -448,6 +448,14 @@ let zencode_string str = "z" ^ List.fold_left (fun s1 s2 -> s1 ^ s2) "" (List.ma
let zencode_upper_string str = "Z" ^ List.fold_left (fun s1 s2 -> s1 ^ s2) "" (List.map zchar (string_to_list str))
+(** Encode string for use as a filename. We can't use zencode directly
+ because some operating systems make the mistake of being
+ case-insensitive. *)
+let file_encode_string str =
+ let zstr = zencode_string str in
+ let md5 = Digest.to_hex (Digest.string zstr) in
+ String.lowercase_ascii zstr ^ String.lowercase_ascii md5
+
let warn str =
if !opt_warnings then
prerr_endline (("Warning" |> yellow |> clear) ^ ": " ^ str)