1 files changed, 1 insertions, 0 deletions
diff --git a/Makefile b/Makefile
index 47f61dbe..0c5b280a 100644
--- a/Makefile
+++ b/Makefile
@@ -202,6 +202,7 @@ compcert.ini: Makefile.config
          echo "arch=$(ARCH)"; \
          echo "model=$(MODEL)"; \
          echo "abi=$(ABI)"; \
+         echo "endianness=$(ENDIANNESS)"; \
          echo "system=$(SYSTEM)"; \
          echo "has_runtime_lib=$(HAS_RUNTIME_LIB)"; \
          echo "has_standard_headers=$(HAS_STANDARD_HEADERS)"; \