# HG changeset patch
# User wenzelm
# Date 1348081595 -7200
# Node ID 8a232a4e3fd88620c81a2574e6554adeeaf8f2d6
# Parent  bec1add86e79e5182774c5b329459936a491ae4d
reactivate HOL-Mirabelle-ex with increased chances that it works most of the time (cf. bec1add86e79, a93d920707bb, be27a453aacc);

diff -r bec1add86e79 -r 8a232a4e3fd8 src/HOL/ROOT
--- a/src/HOL/ROOT	Wed Sep 19 18:01:48 2012 +0200
+++ b/src/HOL/ROOT	Wed Sep 19 21:06:35 2012 +0200
@@ -657,8 +657,8 @@
   theories Mirabelle_Test
 
 session "HOL-Mirabelle-ex" in "Mirabelle/ex" = "HOL-Mirabelle" +
-  options [document = false, timeout = 600 (* FIXME avoid "hang" of external bash *) ]
-  theories [condition = ISABELLE_FULL_TEST] Ex
+  options [document = false, timeout = 60]
+  theories Ex
 
 session "HOL-Word-SMT_Examples" in SMT_Examples = "HOL-Word" +
   options [document = false, quick_and_dirty]