Hi Bruno, On 5/3/24 6:23 AM, Bruno Haible wrote: > Rationale: If there is a problem with the command-line options, > there is a certain probability that the cause is the version > of gnulib-tool. The user may have used an older one, whereas they > intended to use another one. That is, they picked one from the wrong > directory, or a git submodule caused trouble. Omitting the directory > would not helpful for the user's investigation.
Good point. Thanks! Collin
