Fix compilation error on windows.

Authored by dterei on Nov 22 2011, 12:58 PM.

Description

Fix compilation error on windows.

Details

Committed
dtereiNov 22 2011, 12:58 PM
Pushed
bgamariAug 25 2016, 1:39 PM
Parents
rGHCDIFFd45fd800bf43: Update system001 output
Branches
Unknown
Tags
Unknown