+RTS -S slows things down (esp. in parallel), so use +RTS -s instead
authorSimon Marlow <marlowsd@gmail.com>
Fri, 5 Nov 2010 13:27:15 +0000 (13:27 +0000)
committerSimon Marlow <marlowsd@gmail.com>
Fri, 5 Nov 2010 13:27:15 +0000 (13:27 +0000)
runstdtest/runstdtest.prl

index 86f7a71..003e041 100644 (file)
@@ -181,9 +181,9 @@ if ( $SysSpecificTiming =~ /^ghc/ ) {
     } else {
         $cpu_counting_ghc = "";
     }
-    $TimingMagic = "+RTS -S$StatsFile $cpu_counting_ghc -RTS"
+    $TimingMagic = "+RTS -s$StatsFile $cpu_counting_ghc -RTS"
 } elsif ( $SysSpecificTiming eq 'hbc' ) {
-    $TimingMagic = "-S$StatsFile";
+    $TimingMagic = "-s$StatsFile";
 }
 
 if ($PreScript ne '') {