From 1952184634fdde823d7a8782b60e4012f18e7b86 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Sun, 27 Jun 2010 03:38:00 +0000 Subject: [PATCH] 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 --- scripts/run_tests.pl | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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++; -- 2.47.3