On Mon, Dec 10, 2018 at 08:33:25PM -0600, Jacob Bachmeyer wrote: > This patch adds a small note to the manual listing the names of > directories that "getdirs" ignores.
Applied, thanks! Ben
signature.asc
Description: PGP signature
_______________________________________________ DejaGnu mailing list DejaGnu@gnu.org https://lists.gnu.org/mailman/listinfo/dejagnu
