mira.py: building jEdit plugin is required for makeall
authornoschinl
Mon, 14 Jul 2014 15:39:23 +0200
changeset 58901841f41710066
parent 58900 6bb3dd7f8097
child 58902 bc957769b584
mira.py: building jEdit plugin is required for makeall
Admin/mira.py
     1.1 --- a/Admin/mira.py	Tue Jul 15 00:35:07 2014 +0200
     1.2 +++ b/Admin/mira.py	Mon Jul 14 15:39:23 2014 +0200
     1.3 @@ -126,8 +126,11 @@
     1.4      args = (['-o', 'timeout=%s' % timeout] if timeout is not None else []) + list(cmdargs)
     1.5  
     1.6      # invoke build tool
     1.7 -    (return_code, log) = env.run_process('%s/bin/isabelle' % isabelle_home, 'build', '-s', '-v', *args,
     1.8 +    (return_code, log1) = env.run_process('%s/bin/isabelle' % isabelle_home, 'jedit', '-bf',
     1.9              USER_HOME=home_user_dir)
    1.10 +    (return_code, log2) = env.run_process('%s/bin/isabelle' % isabelle_home, 'build', '-s', '-v', *args,
    1.11 +            USER_HOME=home_user_dir)
    1.12 +    log = log1 + log2
    1.13  
    1.14      # collect report
    1.15      return (return_code == 0, extract_isabelle_run_summary(log),