diff options
Diffstat (limited to 'Src/mkmodindex.sh')
| -rw-r--r-- | Src/mkmodindex.sh | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/Src/mkmodindex.sh b/Src/mkmodindex.sh index 75a7e43bc..1f0b8e3bd 100644 --- a/Src/mkmodindex.sh +++ b/Src/mkmodindex.sh @@ -8,6 +8,8 @@ echo "# module index generated by mkmodindex.sh" echo +omit_modules="`echo $OMIT_MODULES | sed 's/,/ /'`" + module_list=' ' while test $# -ne 0; do dir=$1 @@ -27,6 +29,11 @@ while test $# -ne 0; do echo >&2 " (ignoring duplicate)" continue ;; esac + case " $omit_modules " in *" $name "*) + echo >&2 "Module \`$name' found in \$OMIT_MODULES" + echo >&2 " (omitting it)" + continue + ;; esac module_list="$module_list$name " echo "modfile_$q_name=$modfile" eval "modfile_$q_name=\$modfile" |