1 files changed, 1 insertions, 0 deletions

diff --git a/Makefile b/Makefile
index 34a4fd2dbf..f8077975af 100644
--- a/Makefile
+++ b/Makefile
@@ -430,6 +430,7 @@ utils/config.ml: utils/config.mlp config/Makefile
 	    -e 's|%%HOST%%|$(HOST)|' \
 	    -e 's|%%TARGET%%|$(TARGET)|' \
 	    -e 's|%%FLAMBDA%%|$(FLAMBDA)|' \
+	    -e 's|%%SAFE_STRING%%|$(SAFE_STRING)|' \
 	    utils/config.mlp > utils/config.ml
 
 partialclean::