diff options
Diffstat (limited to 'configure')
| -rwxr-xr-x | configure | 20 |
1 files changed, 11 insertions, 9 deletions
diff --git a/configure b/configure index 0584c433f36..55e85474877 100755 --- a/configure +++ b/configure @@ -7850,11 +7850,12 @@ done ac_given_srcdir=$srcdir ac_given_INSTALL="$INSTALL" -trap 'rm -fr `echo "GNUmakefile - src/GNUmakefile - src/Makefile.global - src/backend/port/Makefile - src/test/regress/GNUmakefile +trap 'rm -fr `echo " + GNUmakefile + src/GNUmakefile + src/Makefile.global + src/backend/port/Makefile + src/test/regress/GNUmakefile src/include/config.h" | sed "s/:[^ ]*//g"` conftest*; exit 1' 1 2 15 EOF cat >> $CONFIG_STATUS <<EOF @@ -8011,10 +8012,10 @@ EOF cat >> $CONFIG_STATUS <<EOF CONFIG_FILES=\${CONFIG_FILES-"GNUmakefile - src/GNUmakefile - src/Makefile.global - src/backend/port/Makefile - src/test/regress/GNUmakefile + src/GNUmakefile + src/Makefile.global + src/backend/port/Makefile + src/test/regress/GNUmakefile "} EOF cat >> $CONFIG_STATUS <<\EOF @@ -8231,6 +8232,7 @@ cat >> $CONFIG_STATUS <<EOF EOF cat >> $CONFIG_STATUS <<\EOF +echo timestamp > src/include/stamp-h exit 0 EOF |