diff --git a/bin/install.pike b/bin/install.pike
index 8c7b4a84b0fec2c182997175c466029436f7e027..fd9b2af31f629846ebcd5fd05fe7638c4a697f7b 100644
--- a/bin/install.pike
+++ b/bin/install.pike
@@ -2,7 +2,7 @@
 
 // Pike installer and exporter.
 //
-// $Id: install.pike,v 1.177 2007/07/29 16:11:47 peter Exp $
+// $Id: install.pike,v 1.178 2007/07/29 19:48:27 peter Exp $
 
 #define USE_GTK
 
@@ -2698,6 +2698,10 @@ the PRIVATE_CRT stuff in install.pike.\n");
 				    "modules/dynamic_module_makefile"),
 		       combine_path(include_prefix, 
 				    "modules/dynamic_module_makefile"));
+      low_install_file(combine_path(vars->TMP_BUILDDIR,
+				    "propagated_variables"),
+		       combine_path(include_prefix, 
+				    "propagated_variables"));
       low_install_file(combine_path(vars->SRCDIR,"install-welcome"),
 		       combine_path(prefix, "build/install-welcome"));
       low_install_file(combine_path(vars->SRCDIR,"dumpmaster.pike"),
@@ -2771,6 +2775,11 @@ the PRIVATE_CRT stuff in install.pike.\n");
 		    combine_path(include_prefix,
 				 "modules/dynamic_module_makefile"),
 		    include_prefix);
+      fix_smartlink(combine_path(vars->TMP_BUILDDIR,
+				 "propagated_variables"),
+		    combine_path(include_prefix, 
+				 "propagated_variables"),
+		    include_prefix);
       fix_smartlink(combine_path(vars->TMP_BUILDDIR,"specs"),
 		    combine_path(include_prefix,"specs"), include_prefix);
     }