diff --git a/.gitignore b/.gitignore index 8b53144a7..3b40578fb 100644 --- a/.gitignore +++ b/.gitignore @@ -76,6 +76,7 @@ coqide *~ *# .#* +.*.log *.aux doc/html/ /_CoqProject diff --git a/util/calc_install_files b/util/calc_install_files index 180d0bdcf..daaec3751 100755 --- a/util/calc_install_files +++ b/util/calc_install_files @@ -1,10 +1,11 @@ #!/usr/bin/env bash # The $1 argument of this script should be the desired make target -set -o pipefail - MAKE=${MAKE:-make} -${MAKE} depend >& /dev/null || ${MAKE} depend >&2 -{ ${MAKE} CLIGHTGEN="CLIGHTGEN" -Bn veric floyd $1 2>/dev/null | \ - awk '/^echo COQC /{print $NF}/^CLIGHTGEN/{print $NF}'; } || \ - ${MAKE} CLIGHTGEN="CLIGHTGEN" -Bn veric floyd $1 >&2 +LOG_DEPEND_FILE=${LOG_DEPEND_FILE:-.calc_install_files.depend.log} +LOG_MAKE_FILE=${LOG_MAKE_FILE:-.calc_install_files.make.log} +${MAKE} depend >& "${LOG_DEPEND_FILE}" || \ + { printf "Error in %s: %s\n" "$0" "${MAKE} depend"; cat "${LOG_DEPEND_FILE}"; } >&2 +{ ${MAKE} CLIGHTGEN="CLIGHTGEN" -Bn veric floyd $1 2>"${LOG_MAKE_FILE}" || \ + { printf "Error in %s: %s\n" "$0" "${MAKE} CLIGHTGEN=\"CLIGHTGEN\" -Bn veric floyd"; cat "${LOG_MAKE_FILE}"; } >&2; } | \ + awk '/^echo COQC /{print $NF}/^CLIGHTGEN/{print $NF}'