[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [PATCH] gendocs.sh: default to a common CSS style sheet for HTML out
|
From: |
Karl Berry |
|
Subject: |
Re: [PATCH] gendocs.sh: default to a common CSS style sheet for HTML output |
|
Date: |
Sat, 13 Dec 2014 22:47:39 GMT |
Sorry, I don't want to lose any more of life to CSS debating.
If you want to take over maintenance of gendocs.sh, that would be fine.
Right now the upstream is in Texinfo, but that is historical -- no one
else wanted to maintain it, so I ended up doing so. It could be
maintained as part of guix, or gnulib, or anywhere. I really don't
care. It's a horrible shell script.
karl
- [PATCH] gendocs.sh: default to a common CSS style sheet for HTML output, Ludovic Courtès, 2014/12/11
- Re: [PATCH] gendocs.sh: default to a common CSS style sheet for HTML output, Pádraig Brady, 2014/12/11
- Re: [PATCH] gendocs.sh: default to a common CSS style sheet for HTML output, rekado, 2014/12/11
- Re: [PATCH] gendocs.sh: default to a common CSS style sheet for HTML output, Ludovic Courtès, 2014/12/12
- Re: [PATCH] gendocs.sh: default to a common CSS style sheet for HTML output, rekado, 2014/12/12
- Re: [PATCH] gendocs.sh: default to a common CSS style sheet for HTML output, Ludovic Courtès, 2014/12/12
- Re: [PATCH] gendocs.sh: default to a common CSS style sheet for HTML output, Karl Berry, 2014/12/12
- Re: [PATCH] gendocs.sh: default to a common CSS style sheet for HTML output, Ludovic Courtès, 2014/12/13
- Re: [PATCH] gendocs.sh: default to a common CSS style sheet for HTML output,
Karl Berry <=
Re: [PATCH] gendocs.sh: default to a common CSS style sheet for HTML output, Karl Berry, 2014/12/11