File tree Expand file tree Collapse file tree 2 files changed +8
-6
lines changed Expand file tree Collapse file tree 2 files changed +8
-6
lines changed Original file line number Diff line number Diff line change 7676* ~
7777* #
7878. #*
79+ . * .log
7980* .aux
8081doc /html /
8182/_CoqProject
Original file line number Diff line number Diff line change 11#! /usr/bin/env bash
22# The $1 argument of this script should be the desired make target
33
4- set -o pipefail
5-
64MAKE=${MAKE:- make}
7- ${MAKE} depend >& /dev/null || ${MAKE} depend >&2
8- { ${MAKE} CLIGHTGEN=" CLIGHTGEN" -Bn veric floyd $1 2> /dev/null | \
9- awk ' /^echo COQC /{print $NF}/^CLIGHTGEN/{print $NF}' ; } || \
10- ${MAKE} CLIGHTGEN=" CLIGHTGEN" -Bn veric floyd $1 >&2
5+ LOG_DEPEND_FILE=${LOG_DEPEND_FILE:- .calc_install_files.depend.log}
6+ LOG_MAKE_FILE=${LOG_MAKE_FILE:- .calc_install_files.make.log}
7+ ${MAKE} depend >& " ${LOG_DEPEND_FILE} " || \
8+ { printf " Error in %s: %s\n" " $0 " " ${MAKE} depend" ; cat " ${LOG_DEPEND_FILE} " ; } >&2
9+ { ${MAKE} CLIGHTGEN=" CLIGHTGEN" -Bn veric floyd $1 2> " ${LOG_MAKE_FILE} " || \
10+ { printf " Error in %s: %s\n" " $0 " " ${MAKE} CLIGHTGEN=\" CLIGHTGEN\" -Bn veric floyd" ; cat " ${LOG_MAKE_FILE} " ; } >&2 ; } | \
11+ awk ' /^echo COQC /{print $NF}/^CLIGHTGEN/{print $NF}'
You can’t perform that action at this time.
0 commit comments