diff options
| author | Robert Norton | 2018-05-11 11:31:47 +0100 |
|---|---|---|
| committer | Robert Norton | 2018-05-11 11:31:47 +0100 |
| commit | 619bd9b568f6f8f5691a66602b7635834d3d13a2 (patch) | |
| tree | 42747e95222d1e750a97fb082a6fb4402deba693 /src | |
| parent | 6846d314b5fdc90d7c3a3ee656ebbf12cbdf7f8d (diff) | |
Avoid generating latex files that differ only by case because this causes confusion on case insensitive file systems (e.g. mac).
Diffstat (limited to 'src')
| -rw-r--r-- | src/latex.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/latex.ml b/src/latex.ml index 8688eaa8..3233a4ac 100644 --- a/src/latex.ml +++ b/src/latex.ml @@ -126,11 +126,12 @@ let rec latex_command ?prefix:(prefix="") ?label:(label=None) dir cmd no_loc ((l | Some l -> Printf.sprintf "\\label{%s}" l in let cmd = !opt_prefix_latex ^ prefix ^ cmd in - if StringSet.mem cmd !commands then + let lcmd = String.lowercase cmd in (* lowercase to avoid file names differing only by case *) + if StringSet.mem lcmd !commands then latex_command ~label:label dir (cmd ^ "v") no_loc annot else begin - commands := StringSet.add cmd !commands; + commands := StringSet.add lcmd !commands; let oc = open_out (Filename.concat dir (cmd ^ "_sail.tex")) in output_string oc (Pretty_print_sail.to_string (latex_loc no_loc l)); close_out oc; |
