diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-04-21 16:13:55 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-04-21 16:13:55 +0000 |
| commit | 9b2190b382036354e4ff7026d2cd8f3f4fe8337d (patch) | |
| tree | 3a3c9d6dc424e2c5dae0b09124ecb56ba9c95e09 /driver | |
| parent | 468f0c4407895557ca8089430f894a85f06afe97 (diff) | |
Fixes in PowerPC port
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2209 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'driver')
| -rw-r--r-- | driver/Interp.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/driver/Interp.ml b/driver/Interp.ml index a3ebe80..8d8d8eb 100644 --- a/driver/Interp.ml +++ b/driver/Interp.ml @@ -339,6 +339,7 @@ let do_printf ge m fmt args = Buffer.add_string b (format_float pat (camlfloat_of_coqfloat f)); scan pos' args' | EVlong i :: args', ('d'|'i'|'u'|'o'|'x'|'X') -> + let pat = Str.replace_first (Str.regexp "ll") "" pat in Buffer.add_string b (format_int64 pat (camlint64_of_coqint i)); scan pos' args' | EVptr_global(id, ofs) :: args', 's' -> |