diff options
| -rw-r--r-- | generator/generator_pr.ml | 4 | ||||
| -rw-r--r-- | generator/generator_pr.mli | 2 |
2 files changed, 3 insertions, 3 deletions
diff --git a/generator/generator_pr.ml b/generator/generator_pr.ml index c0a2fb62..fe44ba2d 100644 --- a/generator/generator_pr.ml +++ b/generator/generator_pr.ml @@ -43,7 +43,7 @@ let pr fs = output_string !chan str ) fs -let output_to filename k = +let output_to ?(perm = 0o444) filename k = files := filename :: !files; let filename_new = filename ^ ".new" in @@ -59,7 +59,7 @@ let output_to filename k = (* different, overwrite old one *) (try chmod filename 0o644 with Unix_error _ -> ()); rename filename_new filename; - chmod filename 0o444; + chmod filename perm; printf "written %s\n%!" filename; ) diff --git a/generator/generator_pr.mli b/generator/generator_pr.mli index 47e76c8b..693c6813 100644 --- a/generator/generator_pr.mli +++ b/generator/generator_pr.mli @@ -23,7 +23,7 @@ val pr : ('a, unit, string, unit) format4 -> 'a (** General printing function which prints to the current output file. *) -val output_to : string -> (unit -> unit) -> unit +val output_to : ?perm:int -> string -> (unit -> unit) -> unit (** [output_to filename f] runs [f] and writes the result to [filename]. [filename] is only updated if the output is different from what is in the file already. *) |