Default to bash shell rather than sh for some calls. The call to cat was failing...

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@895 e59a4935-1847-0410-ae03-e826735625c1

diff --git a/scripts/run_tests.pl b/scripts/run_tests.pl
index 2704f61e53b7f882ca2e2e27e725795119b7a759..418f59febea584146c530236fff9ad1550cf2597 100755 (executable)
--- a/scripts/run_tests.pl
+++ b/scripts/run_tests.pl
@@ -267,7 +267,7 @@ $defaultDir =~ s/\n//;
  system("echo Copying to /dev/null to fill the disk cache");
 
  foreach my $testcase (@testcases) {
-  system ("cat " . $testcase . "/*.* > /dev/null");
+  system ("bash", "-c", "cat " . $testcase . "/*.* > /dev/null");
 }
 
 # Total running time
@@ -368,7 +368,7 @@ foreach my $testcase (@testcases) {
        }
        my $time = time;
        # Now, run the sucker
-       my $exitVal = system("$limits; gunzip -f --stdout $file | $timing $stp $stpArgs  $logging");
+       my $exitVal = system("bash", "-c", "$limits; gunzip -f --stdout $file | $timing $stp $stpArgs  $logging");
        $time = time - $time;
        # OK, let's see what happened
        $testsTotal++;