Re: Info-insert-dir

[Richard Stallman]

    I meant `wid-edit' doesn't even check whether it's a "directory name" in
    the sense of a filename ending with a slash (`wid-edit' doesn't
    discriminate directories and files although it provides separate widgets
    for them).

I don't think anything bad happens if you use a file name instead of a
directory name.  It is not "quite right", but it is ok.

It would be a pain in the neck for the `directory' widget to reject
directory file names.

It would be a nice little touch for the `directory' widget
to convert directory file names automatically into directory names.
But let's not change that now.