Commit 4e12b05c authored by Simon Marlow's avatar Simon Marlow

+RTS -S slows things down (esp. in parallel), so use +RTS -s instead

parent cfcf94ae
......@@ -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 '') {
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment