diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2014-12-04 13:12:45 +0100 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2014-12-04 13:12:45 +0100 |
| commit | 5735f427bb0e6698eb946b961baadfed0fac31e5 (patch) | |
| tree | 939d1a2f1bb569c1057107e9760ce800ed235ce6 /powerpc/PrintLinux.ml | |
| parent | 5435a0ac12625b356ecbd9faba1c7ec67f2477a7 (diff) | |
| download | compcert-5735f427bb0e6698eb946b961baadfed0fac31e5.tar.gz compcert-5735f427bb0e6698eb946b961baadfed0fac31e5.zip | |
Changed the d1line and d1file to d2line and d2file and prologue and epilogue printing for printing the line directives without forcing the assembler to generate debug information.
Diffstat (limited to 'powerpc/PrintLinux.ml')
| -rw-r--r-- | powerpc/PrintLinux.ml | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/powerpc/PrintLinux.ml b/powerpc/PrintLinux.ml index 593b6413..ed4ef19b 100644 --- a/powerpc/PrintLinux.ml +++ b/powerpc/PrintLinux.ml @@ -110,5 +110,11 @@ module Linux_System = let print_prologue oc = () + + let print_epilogue oc = () + + let set_compilation_unit_addrs _ _ = () + + let print_addr_label _ _ = () end:SYSTEM) |