diff options
Diffstat (limited to 'scripts/dhall_check.sh')
-rwxr-xr-x | scripts/dhall_check.sh | 24 |
1 files changed, 9 insertions, 15 deletions
diff --git a/scripts/dhall_check.sh b/scripts/dhall_check.sh index a3413ec..5a1ee1b 100755 --- a/scripts/dhall_check.sh +++ b/scripts/dhall_check.sh | |||
@@ -1,25 +1,19 @@ | |||
1 | #!/usr/bin/env bash | 1 | #!/usr/bin/env bash |
2 | 2 | ||
3 | pushd () { | 3 | set -eo pipefail |
4 | command pushd "$@" > /dev/null | ||
5 | } | ||
6 | |||
7 | popd () { | ||
8 | command popd "$@" > /dev/null | ||
9 | } | ||
10 | 4 | ||
11 | go() { | 5 | go() { |
12 | local ERROR=0; | 6 | local ERROR=0 |
13 | for file in $(find -type f -name "*.dhall"); do | 7 | while IFS= read -r -d '' file |
14 | pushd $(dirname $file); | 8 | do |
15 | cat $(basename $file) | dhall --explain resolve > /dev/null; | 9 | cd "$(dirname "$file")" || exit |
16 | echo "Typechecking ${file}" | 10 | echo "Typechecking ${file}" |
17 | if [ "$?" -ne "0" ]; then | 11 | if ! dhall --explain resolve < "$(basename "$file")" >/dev/null; then |
18 | echo "Failed to resolve $file" | 12 | echo "Failed to resolve $file" |
19 | ERROR=1; | 13 | ERROR=1 |
20 | fi; | 14 | fi; |
21 | popd; | 15 | cd - >/dev/null || exit |
22 | done; | 16 | done < <(find . -type f -name "*.dhall" -print0) |
23 | exit $ERROR; | 17 | exit $ERROR; |
24 | } | 18 | } |
25 | 19 | ||