diff --git a/configure b/configure index 8010d4221..43294bb68 100755 --- a/configure +++ b/configure @@ -5255,6 +5255,7 @@ fi; done EOF cat >> $CONFIG_STATUS <> $CONFIG_STATUS <<\EOF test -z "$CONFIG_HEADERS" || echo timestamp > libguile/stamp-h