summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorRobert Norton2018-05-11 11:32:31 +0100
committerRobert Norton2018-05-11 11:32:31 +0100
commit17c786ea27bf644efdae271b8a93bd5ce1d730e8 (patch)
treec09e991535a7a9092b36e17fd75103b10d0fdfd8
parent619bd9b568f6f8f5691a66602b7635834d3d13a2 (diff)
Remove unneeded _sail suffix from latex files.
-rw-r--r--src/latex.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/latex.ml b/src/latex.ml
index 3233a4ac..0520d074 100644
--- a/src/latex.ml
+++ b/src/latex.ml
@@ -132,10 +132,10 @@ let rec latex_command ?prefix:(prefix="") ?label:(label=None) dir cmd no_loc ((l
else
begin
commands := StringSet.add lcmd !commands;
- let oc = open_out (Filename.concat dir (cmd ^ "_sail.tex")) in
+ let oc = open_out (Filename.concat dir (cmd ^ ".tex")) in
output_string oc (Pretty_print_sail.to_string (latex_loc no_loc l));
close_out oc;
- string (Printf.sprintf "\\newcommand{\\%s}{%s " cmd labelling) ^^ (docstring l) ^^ string (Printf.sprintf "\\lstinputlisting[language=sail]{%s/%s_sail.tex}}" dir cmd)
+ string (Printf.sprintf "\\newcommand{\\%s}{%s " cmd labelling) ^^ (docstring l) ^^ string (Printf.sprintf "\\lstinputlisting[language=sail]{%s/%s.tex}}" dir cmd)
end
let latex_command_id ?prefix:(prefix="") dir id no_loc annot =