diff options
Diffstat (limited to 'Build/source/configure')
| -rwxr-xr-x | Build/source/configure | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/Build/source/configure b/Build/source/configure index 8af05266bb4..f4dabdf78f7 100755 --- a/Build/source/configure +++ b/Build/source/configure @@ -21140,7 +21140,7 @@ fi subdirs="$subdirs auxdir/auxsub libs utils texk" -ac_config_files="$ac_config_files Makefile" +ac_config_files="$ac_config_files Makefile doc/Makefile" rm -f Makefile @@ -22280,6 +22280,7 @@ do "depfiles") CONFIG_COMMANDS="$CONFIG_COMMANDS depfiles" ;; "libtool") CONFIG_COMMANDS="$CONFIG_COMMANDS libtool" ;; "Makefile") CONFIG_FILES="$CONFIG_FILES Makefile" ;; + "doc/Makefile") CONFIG_FILES="$CONFIG_FILES doc/Makefile" ;; *) as_fn_error $? "invalid argument: \`$ac_config_target'" "$LINENO" 5;; esac |