# deal with system-specific timing options
$TimingMagic = '';
if ( $SysSpecificTiming =~ /^ghc/ ) {
- $TimingMagic = "+RTS -s$StatsFile -RTS"
+ $TimingMagic = "+RTS -S$StatsFile -RTS"
} elsif ( $SysSpecificTiming eq 'hbc' ) {
$TimingMagic = "-S$StatsFile";
}