# HG changeset patch
# User wenzelm
# Date 1576704381 -3600
# Node ID 64ec254d901d126a3728685c5f4187fdf19e323a
# Parent  5b68cc73f8b198a58913ae142326d404939f8d00
proper backup;

diff -r 5b68cc73f8b1 -r 64ec254d901d 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 =