diff options
Diffstat (limited to 'gen_links.sh.inc')
| -rw-r--r-- | gen_links.sh.inc | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/gen_links.sh.inc b/gen_links.sh.inc index 539b3983..f1344278 100644 --- a/gen_links.sh.inc +++ b/gen_links.sh.inc @@ -16,6 +16,8 @@ # See the License for the specific language governing permissions and # limitations under the License. +set -e + rm -f .gitignore gen_link() { @@ -36,6 +38,8 @@ gen_links() { } ignore_pp_results() { + # Avoid using the pattern itself if no file is found in globbing below: + shopt -s nullglob for pp in *.ttcnpp; do ttcn_file="$(echo $pp | sed 's/pp$//')" echo "$ttcn_file" >> .gitignore |