diff options
Diffstat (limited to 'powerpc')
-rw-r--r-- | powerpc/PrintAsm.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml index 3ef3c744..a20448c3 100644 --- a/powerpc/PrintAsm.ml +++ b/powerpc/PrintAsm.ml @@ -747,6 +747,10 @@ let print_instruction oc tbl pc = function (Int32.to_int (camlint_of_coqint al)) args | EF_annot_val(txt, targ) -> print_annot_val oc (extern_atom txt) args res + | EF_inline_asm txt -> + fprintf oc "%s begin inline assembly\n" comment; + fprintf oc " %s\n" (extern_atom txt); + fprintf oc "%s end inline assembly\n" comment | _ -> assert false end |