Guillermo Rodriguez <guillerodriguez.dev at gmail.com> writes: > 2017-06-25 21:10 GMT+02:00 David Kastrup <dak at gnu.org>: >> David Kastrup <dak at gnu.org> writes: [...] > Also looks like a cosmetic indentation issue, no actual problems. > > The fixes for both are trivial, I am submitting them separately. Thanks! -- David Kastrup