# HG changeset patch
# User wenzelm
# Date 1543836637 -3600
# Node ID fe2c16d9367a8f027298ea7d2177d01046fd9bd2
# Parent  a3c776b9d3dd7254bef960a47d5e1aab7c987a85
tuned;

diff -r a3c776b9d3dd -r fe2c16d9367a src/Pure/Admin/build_release.scala
--- a/src/Pure/Admin/build_release.scala	Sun Dec 02 21:59:03 2018 +0100
+++ b/src/Pure/Admin/build_release.scala	Mon Dec 03 12:30:37 2018 +0100
@@ -67,17 +67,18 @@
     {
       change_file(dir, name,
         s =>
-          s.replaceAll("val is_identified = false", "val is_identified = true")
-           .replaceAll("val is_official = false", "val is_official = " + is_official))
+          s.replaceAllLiterally("val is_identified = false", "val is_identified = true")
+           .replaceAllLiterally("val is_official = false", "val is_official = " + is_official))
     }
 
     change_file(dir, getsettings_file,
       s =>
-        s.replaceAll("ISABELLE_ID=\"\"", "ISABELLE_ID=" + quote(release.ident))
-         .replaceAll("ISABELLE_IDENTIFIER=\"\"", "ISABELLE_IDENTIFIER=" + quote(release.dist_name)))
+        s.replaceAllLiterally("ISABELLE_ID=\"\"", "ISABELLE_ID=" + quote(release.ident))
+         .replaceAllLiterally("ISABELLE_IDENTIFIER=\"\"",
+            "ISABELLE_IDENTIFIER=" + quote(release.dist_name)))
 
     change_file(dir, "lib/html/library_index_header.template",
-      s => s.replaceAll("""\{ISABELLE\}""", release.dist_name))
+      s => s.replaceAllLiterally("{ISABELLE}", release.dist_name))
 
     for {
       name <-
@@ -86,11 +87,12 @@
           "src/Pure/System/distribution.scala",
           "lib/Tools/version") }
     {
-      change_file(dir, name, s => s.replaceAll("repository version", release.dist_version))
+      change_file(dir, name,
+        s => s.replaceAllLiterally("repository version", release.dist_version))
     }
 
     change_file(dir, "README",
-      s => s.replaceAll("some repository version of Isabelle", release.dist_version))
+      s => s.replaceAllLiterally("some repository version of Isabelle", release.dist_version))
   }