From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Sun, 27 Jun 2010 03:38:00 +0000 (+0000)
Subject: Default to bash shell rather than sh for some calls. The call to cat was failing... 
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=1952184634fdde823d7a8782b60e4012f18e7b86;p=francis%2Fstp.git

Default to bash shell rather than sh for some calls. The call to cat was failing on a redhat machine with an "argument too long error". Hopefully this fixes it.

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 2704f61..418f59f 100755
--- 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++;