File tree 2 files changed +8
-6
lines changed
2 files changed +8
-6
lines changed Original file line number Diff line number Diff line change 76
76
* ~
77
77
* #
78
78
. # *
79
+ . * .log
79
80
* .aux
80
81
doc /html /
81
82
/_CoqProject
Original file line number Diff line number Diff line change 1
1
#! /usr/bin/env bash
2
2
# The $1 argument of this script should be the desired make target
3
3
4
- set -o pipefail
5
-
6
4
MAKE=${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 $1 " ; 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