diff options
| -rwxr-xr-x | Tools/scripts/redundant-opt-files.sh | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/Tools/scripts/redundant-opt-files.sh b/Tools/scripts/redundant-opt-files.sh index 6d028f153e1a..505afc62db02 100755 --- a/Tools/scripts/redundant-opt-files.sh +++ b/Tools/scripts/redundant-opt-files.sh @@ -38,6 +38,11 @@ catport() { identical_options() { local origin=$(catport $1) + if [ ! -d ${origin} ]; then + # origin no longer exists, list it anyway without testing further + echo ${origin} + return + fi local selected_pristine=$(/usr/bin/make -C ${origin} \ -V SELECTED_OPTIONS PORT_DBDIR=/dev/null) local selected_now=$(/usr/bin/make -C ${origin} -V SELECTED_OPTIONS) |