# HG changeset patch # User noschinl # Date 1405345163 -7200 # Node ID 841f41710066a4c55be0f27fc6e8956c5526ab84 # Parent 6bb3dd7f8097eadfe8b1ccc01d5e74150ac8f983 mira.py: building jEdit plugin is required for makeall diff -r 6bb3dd7f8097 -r 841f41710066 Admin/mira.py --- a/Admin/mira.py Tue Jul 15 00:35:07 2014 +0200 +++ b/Admin/mira.py Mon Jul 14 15:39:23 2014 +0200 @@ -126,8 +126,11 @@ args = (['-o', 'timeout=%s' % timeout] if timeout is not None else []) + list(cmdargs) # invoke build tool - (return_code, log) = env.run_process('%s/bin/isabelle' % isabelle_home, 'build', '-s', '-v', *args, + (return_code, log1) = env.run_process('%s/bin/isabelle' % isabelle_home, 'jedit', '-bf', USER_HOME=home_user_dir) + (return_code, log2) = env.run_process('%s/bin/isabelle' % isabelle_home, 'build', '-s', '-v', *args, + USER_HOME=home_user_dir) + log = log1 + log2 # collect report return (return_code == 0, extract_isabelle_run_summary(log),