# HG changeset patch
# User wenzelm
# Date 1455224712 -3600
# Node ID 45adb8dc84e1279f415cc00ee7c5e0a542fd339e
# Parent  707f9b182f4fb4c02048e910f3bac7197971d4e3
invoke perl system with explicit list -- to avoid extra /bin/sh and thus evade potential conflict of /bin/sh -> dash with bash on Debian/Ubuntu;

diff -r 707f9b182f4f -r 45adb8dc84e1 src/HOL/Mirabelle/lib/scripts/mirabelle.pl
--- a/src/HOL/Mirabelle/lib/scripts/mirabelle.pl	Thu Feb 11 16:29:38 2016 +0100
+++ b/src/HOL/Mirabelle/lib/scripts/mirabelle.pl	Thu Feb 11 22:05:12 2016 +0100
@@ -157,8 +157,11 @@
 
 if ($output_log) { print "Mirabelle: $thy_file\n"; }
 
-my $result = system "\"$ENV{'ISABELLE_PROCESS'}\" " .
-  "-o quick_and_dirty -e 'Multithreading.max_threads_setmp 1 use_thy \"$path/$new_thy_name\" handle _ => exit 1;\n' -q $mirabelle_logic" . $quiet;
+my $cmd =
+  "\"$ENV{'ISABELLE_PROCESS'}\" " .
+  "-o quick_and_dirty -e 'Multithreading.max_threads_setmp 1 use_thy \"$path/$new_thy_name\" handle _ => exit 1;\n' -q $mirabelle_logic" .
+  $quiet;
+my $result = system "bash", "-c", $cmd;
 
 if ($output_log) {
   my $outcome = ($result ? "failure" : "success");