diff --git a/gen_links.sh.inc b/gen_links.sh.inc index 539b3983d..c21bcd60d 100644 --- a/gen_links.sh.inc +++ b/gen_links.sh.inc @@ -36,6 +36,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