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'