# HG changeset patch
# User wenzelm
# Date 1475657032 -7200
# Node ID 5a6a7401c48b983bc42bdf2cd8a0e470938d0275
# Parent  c6160d0b0337948d15ad5dab5d890db7a0535995
clarified sanity checks;

diff -r c6160d0b0337 -r 5a6a7401c48b src/Pure/Tools/build_history.scala
--- a/src/Pure/Tools/build_history.scala	Tue Oct 04 21:11:35 2016 +0200
+++ b/src/Pure/Tools/build_history.scala	Wed Oct 05 10:43:52 2016 +0200
@@ -44,6 +44,9 @@
 
     /* sanity checks */
 
+    if (File.eq(Path.explode("~~").file, hg.root.file))
+      error("Repository coincides with ISABELLE_HOME=" + Path.explode("~~").expand)
+
     if (threads < 1) error("Bad threads value < 1: " + threads)
 
     if (heap < 100) error("Bad heap value < 100: " + heap)
@@ -189,7 +192,6 @@
   def main(args: Array[String])
   {
     Command_Line.tool0 {
-      var allow = false
       var components_base = ""
       var heap: Option[Int] = None
       var max_heap: Option[Int] = None
@@ -206,7 +208,6 @@
 Usage: isabelle build_history [OPTIONS] REPOSITORY [ARGS ...]
 
   Options are:
-    -A           allow irreversible cleanup of REPOSITORY clone (required)
     -C DIR       base directory for Isabelle components (default: $ISABELLE_HOME_USER/../contrib)
     -H SIZE      minimal ML heap in MB (default: """ + default_heap + """ for x86, """ + default_heap * 2 + """ for x86_64)
     -M THREADS   number of threads for Poly/ML RTS and Isabelle/ML (default: """ + default_threads + """)
@@ -222,7 +223,6 @@
   Build Isabelle sessions from the history of another REPOSITORY clone,
   passing ARGS directly to its isabelle build tool.
 """,
-        "A" -> (_ => allow = true),
         "C:" -> (arg => components_base = arg),
         "H:" -> (arg => heap = Some(Value.Int.parse(arg))),
         "M:" -> (arg => threads = Value.Int.parse(arg)),
@@ -249,10 +249,6 @@
 
       using(Mercurial.open_repository(Path.explode(root)))(hg =>
         {
-          if (!allow)
-            error("Repository " + hg + " will be cleaned thoroughly!\n" +
-              "Provide option -A to allow this explicitly.")
-
           val progress = new Console_Progress(false)
           val res =
             build_history(progress, hg, rev = rev, isabelle_identifier = isabelle_identifier,