# 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,