Use +RTS -S<file> rather than +RTS -s<file>, since the latter only
gives summary statistics now.
# deal with system-specific timing options
$TimingMagic = '';
if ( $SysSpecificTiming =~ /^ghc/ ) {
# 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";
}
} elsif ( $SysSpecificTiming eq 'hbc' ) {
$TimingMagic = "-S$StatsFile";
}