1 files changed, 1 insertions, 0 deletions
diff --git a/Makefile b/Makefile
index fd0595d4..62635d70 100644
--- a/Makefile
+++ b/Makefile
@@ -297,6 +297,7 @@ compcert.ini: Makefile.config
 	 echo "linker_options=$(CLINKER_OPTIONS)";\
          echo "arch=$(ARCH)"; \
          echo "model=$(MODEL)"; \
+	       echo "os=$(OS)"; \
          echo "abi=$(ABI)"; \
          echo "endianness=$(ENDIANNESS)"; \
          echo "system=$(SYSTEM)"; \