From be4d6e42dfa287b93b1a35ec820ab2a5aaf8c7ec Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Sun, 19 May 2013 09:54:40 +0000
Subject: Merge of the float32 branch: - added RTL type "Tsingle" -
 ABI-compatible passing of single-precision floats on ARM and x86

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2260 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 backend/PrintXTL.ml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'backend/PrintXTL.ml')

diff --git a/backend/PrintXTL.ml b/backend/PrintXTL.ml
index 756fc58c..258babaf 100644
--- a/backend/PrintXTL.ml
+++ b/backend/PrintXTL.ml
@@ -29,7 +29,11 @@ let mreg pp r =
   | Some s -> fprintf pp "%s" s
   | None -> fprintf pp "<unknown machreg>"
 
-let short_name_of_type = function Tint -> 'i' | Tfloat -> 'f' | Tlong -> 'l'
+let short_name_of_type = function
+  | Tint -> 'i'
+  | Tfloat -> 'f'
+  | Tlong -> 'l'
+  | Tsingle -> 's'
 
 let loc pp = function
   | R r -> mreg pp r
-- 
cgit