From f50a1c1e1dc194c78b68ecdc7e3f6c0b0448f5f4 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Sat, 11 Apr 2020 10:29:45 +0200 Subject: seems like the ARM profiling perhaps works --- backend/PrintAsmaux.ml | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) (limited to 'backend/PrintAsmaux.ml') diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml index c7161615..cc7b33c3 100644 --- a/backend/PrintAsmaux.ml +++ b/backend/PrintAsmaux.ml @@ -358,11 +358,7 @@ let write_symbol_pointer oc sym = then fprintf oc " .8byte %s\n" sym else fprintf oc " .4byte %s\n" sym;; -let declare_function oc name = - fprintf oc " .type %s, @function\n" name; - fprintf oc " .size %s, . - %s\n" name name;; - -let print_profiling_epilogue finalizer_call_method print_profiling_stub oc = +let print_profiling_epilogue declare_function finalizer_call_method print_profiling_stub oc = let nr_items = !next_profiling_position in if nr_items > 0 then -- cgit