Skip to content

Commit

Permalink
Use log files instead of re-running commands in calc_install_files
Browse files Browse the repository at this point in the history
  • Loading branch information
JasonGross committed Aug 29, 2023
1 parent 85e940d commit e3da59b
Show file tree
Hide file tree
Showing 2 changed files with 8 additions and 6 deletions.
1 change: 1 addition & 0 deletions .gitignore
Original file line number Diff line number Diff line change
Expand Up @@ -76,6 +76,7 @@ coqide
*~
*#
.#*
.*.log
*.aux
doc/html/
/_CoqProject
Expand Down
13 changes: 7 additions & 6 deletions util/calc_install_files
Original file line number Diff line number Diff line change
@@ -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}'

0 comments on commit e3da59b

Please sign in to comment.