proper backup;
authorwenzelm
Wed, 18 Dec 2019 22:26:21 +0100
changeset 71315 64ec254d901d
parent 71314 5b68cc73f8b1
child 71316 3fc2def62547
proper backup;
src/Pure/General/mercurial.scala
--- a/src/Pure/General/mercurial.scala	Wed Dec 18 21:28:50 2019 +0100
+++ b/src/Pure/General/mercurial.scala	Wed Dec 18 22:26:21 2019 +0100
@@ -194,7 +194,7 @@
 
     def commit(lines: List[String]): Boolean =
     {
-      File.write(hgrc, cat_lines(lines))
+      File.write_backup(hgrc, cat_lines(lines))
       true
     }
     val edited =