]> matita.cs.unibo.it Git - helm.git/blobdiff - components/xml/xml.ml
fixed some file permissions (anybody can rebuild a published devel)
[helm.git] / components / xml / xml.ml
index f8cc41cbeacb7d3404c9548b9932d9565b8c4262..0e3a4bcc24a91fbb447869ce8bdbebe64593e076 100644 (file)
@@ -123,23 +123,27 @@ let pp ?(gzip=false) strm fn =
     match fn with
     | Some filename ->
         let outchan = Gzip.open_out filename in
-        (try
+        begin try
           pp_to_gzipchan strm outchan;
         with e ->
           Gzip.close_out outchan;
-          raise e);
-        Gzip.close_out outchan
+          raise e
+       end;
+        Gzip.close_out outchan;
+       HExtlib.chmod 0o664 filename;
     | None -> failwith "Can't sent gzipped output to stdout"
   else
     match fn with
     | Some filename ->
         let outchan = open_out filename in
-        (try
+        begin try
           pp_to_outchan strm outchan;
         with e ->
           close_out outchan;
-          raise e);
-        close_out outchan
+          raise e
+       end;
+        close_out outchan;
+       HExtlib.chmod 0o664 filename
     | None -> pp_to_outchan strm stdout
 ;;