# HG changeset patch
# User wenzelm
# Date 1347889096 -7200
# Node ID a93d920707bb54415682c34530ed246360089766
# Parent  caea18a5265fde8e1e8567623cf7ffb8f722b3ae
bypass HOL-Mirabelle-ex in regular test, until its tendency to "hang" has been resolved;

diff -r caea18a5265f -r a93d920707bb src/HOL/ROOT
--- a/src/HOL/ROOT	Mon Sep 17 15:33:22 2012 +0200
+++ b/src/HOL/ROOT	Mon Sep 17 15:38:16 2012 +0200
@@ -658,7 +658,7 @@
 
 session "HOL-Mirabelle-ex" in "Mirabelle/ex" = "HOL-Mirabelle" +
   options [document = false, timeout = 600 (* FIXME avoid "hang" of external bash *) ]
-  theories Ex
+  theories [condition = ISABELLE_FULL_TEST] Ex
 
 session "HOL-Word-SMT_Examples" in SMT_Examples = "HOL-Word" +
   options [document = false, quick_and_dirty]