From 73948e54a63eac456430eae66fc05880466d7203 Mon Sep 17 00:00:00 2001 From: "John J. Camilleri" Date: Thu, 9 Aug 2018 10:05:10 +0200 Subject: [PATCH] Make.sh: halt on error, skip non-existant files Was trying to compile src/*/SymbolHeb.gf which doesn't exist --- Make.sh | 2 ++ 1 file changed, 2 insertions(+) diff --git a/Make.sh b/Make.sh index ce194b44..30a8bfc8 100755 --- a/Make.sh +++ b/Make.sh @@ -3,6 +3,7 @@ # --- # Non-Haskell RGL build script for Unix-based machines # --- +set -e # Get languages from config langs=$(tail -n +2 languages.csv | awk -F ',' '{ if ($6 != "n") { print $1 } }') @@ -73,6 +74,7 @@ for lang in $langs; do if [ $mod == "Try" ] && [[ "$langs_try" != *"$lang"* ]]; then continue; fi if [ $mod == "Symbolic" ] && [[ "$langs_symbolic" != *"$lang"* ]]; then continue; fi for file in "${src}"/*/"${mod}${lang}".gf; do + if [ ! -f "$file" ]; then continue; fi if [[ "$langs_present" = *"$lang"* ]]; then modules_present="${modules_present} ${file}"; fi modules_alltenses="${modules_alltenses} ${file}" done