Hi Andy, > >> > diff --git a/.gitignore b/.gitignore > >> > index 3deeab2..bce9756 100644 > >> > --- a/.gitignore > >> > +++ b/.gitignore > >> > @@ -13,6 +13,7 @@ config.status > >> > config.log > >> > config.h > >> > *.doc > >> > +*.html > >> > *.x > >> > *.lo > >> > *.la
> >> Can you make it more specific please? I.e. doc/ref/guile.html > > Is this what you meant ? If so it can be applied to master as well > No, like /doc/ref/guile.html in the root .gitignore please; see other > similar lines in the root gitignore. I'm sorry for so many email for such a tiny patch, but there is no html related entry in the top level .gitignore :), but instead, a doc/ref/.gitignore ... [which explains my first and second patch 'offer']. I can of course move its content to the top level [updating for respective path of course], remove this file and add an entry for r5rs html doc Please confirm and I'll do that. Cheers, David
pgpSqXPbXRuVO.pgp
Description: OpenPGP digital signature
