diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-08-17 14:24:34 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-08-17 14:24:34 +0000 |
| commit | 2199fd1838ab1c32d55c760e92b97077d8eaae50 (patch) | |
| tree | 1f82bf1de35a821e065403dd510f54510627aa66 /powerpc/PrintAsm.ml | |
| parent | 4b119d6f9f0e846edccaf5c08788ca1615b22526 (diff) | |
| download | compcert-2199fd1838ab1c32d55c760e92b97077d8eaae50.tar.gz compcert-2199fd1838ab1c32d55c760e92b97077d8eaae50.zip | |
Refactored Selection.v and Selectionproof.v into a machine-dependent part + a machine-independent part.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1125 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'powerpc/PrintAsm.ml')
| -rw-r--r-- | powerpc/PrintAsm.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml index aa327731..e86b7dc4 100644 --- a/powerpc/PrintAsm.ml +++ b/powerpc/PrintAsm.ml @@ -182,8 +182,8 @@ let (text, data, const_data, float_literal) = | Diab -> (".text", ".data", - ".const", (* to check *) - ".const") (* to check *) + ".data", (* to check *) + ".data") (* to check *) (* Encoding masks for rlwinm instructions *) |