# HG changeset patch
# User wenzelm
# Date 1411415159 -7200
# Node ID e4d540c0dd57509c14c980ecb319d89a8085af7a
# Parent  b5d27faef560669405eb099b624dbc9b5c84275e
clarified timeout for isatest;

diff -r b5d27faef560 -r e4d540c0dd57 Admin/isatest/isatest-makeall
--- a/Admin/isatest/isatest-makeall	Mon Sep 22 21:31:45 2014 +0200
+++ b/Admin/isatest/isatest-makeall	Mon Sep 22 21:45:59 2014 +0200
@@ -87,10 +87,10 @@
 
     case "$SETTINGS" in
       *sml*)
-        BUILD_ARGS="-o timeout=36000 $BUILD_ARGS"
+        BUILD_ARGS="-o timeout=54000 $BUILD_ARGS"
         ;;
       *)
-        BUILD_ARGS="-o timeout=3600 $BUILD_ARGS"
+        BUILD_ARGS="-o timeout=5400 $BUILD_ARGS"
         ;;
     esac
 
diff -r b5d27faef560 -r e4d540c0dd57 src/HOL/ROOT
--- a/src/HOL/ROOT	Mon Sep 22 21:31:45 2014 +0200
+++ b/src/HOL/ROOT	Mon Sep 22 21:45:59 2014 +0200
@@ -19,7 +19,7 @@
   description {*
     HOL-Main with explicit proof terms.
   *}
-  options [timeout = 5400, document = false]
+  options [document = false]
   theories Proofs (*sequential change of global flag!*)
   theories "~~/src/HOL/Library/Old_Datatype"
   files
@@ -260,7 +260,7 @@
 
     Testing Metis and Sledgehammer.
   *}
-  options [timeout = 3600, document = false]
+  options [document = false]
   theories
     Abstraction
     Big_O
@@ -522,7 +522,7 @@
   description {*
     Miscellaneous examples for Higher-Order Logic.
   *}
-  options [timeout = 3600, condition = ML_SYSTEM_POLYML]
+  options [condition = ML_SYSTEM_POLYML]
   theories [document = false]
     "~~/src/HOL/Library/State_Monad"
     Code_Binary_Nat_examples
@@ -722,7 +722,7 @@
   theories Nominal
 
 session "HOL-Nominal-Examples" in "Nominal/Examples" = "HOL-Nominal" +
-  options [timeout = 3600, condition = ML_SYSTEM_POLYML, document = false]
+  options [condition = ML_SYSTEM_POLYML, document = false]
   theories
     Nominal_Examples_Base
   theories [condition = ISABELLE_FULL_TEST]