# HG changeset patch
# User krauss
# Date 1299235974 -3600
# Node ID 7c4a4b02dbdb108e71010d39bf64a0767330ea4e
# Parent  dde7df1176b780af1fab355cd14bdee42ffa7534
produce helpful mira summary for more errors

diff -r dde7df1176b7 -r 7c4a4b02dbdb Admin/mira.py
--- a/Admin/mira.py	Fri Mar 04 00:09:47 2011 +0100
+++ b/Admin/mira.py	Fri Mar 04 11:52:54 2011 +0100
@@ -79,7 +79,7 @@
 
 def extract_isabelle_run_summary(logdata):
 
-    re_error = re.compile(r'^\*\*\* (.*)$', re.MULTILINE)
+    re_error = re.compile(r'^(?:make: )?\*\*\* (.*)$', re.MULTILINE)
     summary = '\n'.join(re_error.findall(logdata))
     if summary == '':
         summary = 'ok'