equal
deleted
inserted
replaced
136 } |
136 } |
137 |
137 |
138 if ($output_log) { print "Mirabelle: $thy_file\n"; } |
138 if ($output_log) { print "Mirabelle: $thy_file\n"; } |
139 |
139 |
140 my $result = system "\"$ENV{'ISABELLE_PROCESS'}\" " . |
140 my $result = system "\"$ENV{'ISABELLE_PROCESS'}\" " . |
141 "-e 'use_thy \"$path/$new_thy_name\" handle _ => exit 1;\n' -q $mirabelle_logic" . $quiet; |
141 "-e 'Unsynchronized.setmp quick_and_dirty true use_thy \"$path/$new_thy_name\" handle _ => exit 1;\n' -q $mirabelle_logic" . $quiet; |
142 |
142 |
143 if ($output_log) { print "Finished: $thy_file\n"; } |
143 if ($output_log) { print "Finished: $thy_file\n"; } |
144 |
144 |
145 |
145 |
146 # cleanup |
146 # cleanup |