Re: recommendations for use of gnulib-tool

[Karl Berry]

Hi Bruno,

    Here is a suggested change
    to the hello/README-dev file.

Since all the kings have seemingly left the building, I made a similar
change on their behalf.  Thanks from all :).