diff -r 26614beb3529 -r 1e2e68984a9f src/Pure/General/mercurial.scala
--- a/src/Pure/General/mercurial.scala	Thu Dec 19 15:55:52 2019 +0100
+++ b/src/Pure/General/mercurial.scala	Thu Dec 19 16:16:49 2019 +0100
@@ -194,7 +194,7 @@
 
     def commit(lines: List[String]): Boolean =
     {
-      File.write_backup(hgrc, cat_lines(lines))
+      File.write(hgrc, cat_lines(lines))
       true
     }
     val edited =
@@ -203,9 +203,11 @@
         lines.filter(header).length == 1 && {
           if (local_hg.paths(options = "-q").contains(path_name)) {
             val old_source = local_hg.paths(args = path_name).head
+            val old_entry = path_name + ".old = " + old_source
             val lines1 =
               lines.map {
-                case Entry(a, b) if a == path_name && b == old_source => new_entry
+                case Entry(a, b) if a == path_name && b == old_source =>
+                  new_entry + "\n" + old_entry
                 case line => line
               }
             lines != lines1 && commit(lines1)