diff options
Diffstat (limited to 'Makefile')
-rw-r--r-- | Makefile | 2 |
1 files changed, 0 insertions, 2 deletions
@@ -225,8 +225,6 @@ compcert.ini: Makefile.config echo "has_runtime_lib=$(HAS_RUNTIME_LIB)"; \ echo "has_standard_headers=$(HAS_STANDARD_HEADERS)"; \ echo "asm_supports_cfi=$(ASM_SUPPORTS_CFI)"; \ - echo "struct_passing_style=$(STRUCT_PASSING)"; \ - echo "struct_return_style=$(STRUCT_RETURN)"; \ echo "response_file_style=$(RESPONSEFILE)";) \ > compcert.ini |