Andreas Schwab <schwab@suse.de> writes:

> > What is the WAIS format, and is it still relevant?
>
> https://en.wikipedia.org/wiki/Wide_area_information_server

I figured it was something like that.  I doubt many users would even
know what that is nowadays.

Does anyone object to the attached patch?

Thanks,
Stefan Kangas