+# gdb depends on gnulib, but as nothing else does, only include it if
+# gdb is built.
+if echo " ${configdirs} " | grep " gdb " > /dev/null 2>&1 ; then
+ # The Makefile provides the ordering, so it's enough here to add
+ # gnulib to the list.
+ configdirs="${configdirs} gnulib"
+fi
+