diff options
Diffstat (limited to 'src/sail.ml')
| -rw-r--r-- | src/sail.ml | 12 |
1 files changed, 10 insertions, 2 deletions
diff --git a/src/sail.ml b/src/sail.ml index 65473d86..006c0e58 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -310,8 +310,16 @@ let main() = (if !(opt_print_latex) then begin - let out = match !opt_file_out with None -> "out.tex" | Some s -> s ^ ".tex" in - let chan = open_out out in + let latex_dir = match !opt_file_out with None -> "sail_latex" | Some s -> s in + try + if not (Sys.is_directory latex_dir) then begin + prerr_endline ("Failure: latex output directory exists but is not a directory: " ^ latex_dir); + exit 1 + end + with Sys_error(_) -> Unix.mkdir latex_dir 0o755; + Sys.chdir latex_dir; + let chan = open_out "commands.tex" in + Latex.latex_dir := latex_dir; output_string chan (Pretty_print_sail.to_string (Latex.latex_defs ast)); close_out chan end |