* gcc.gnu.org += makeinfo
@ 2020-03-09 9:47 Gerald Pfeifer
2020-03-09 13:25 ` Frank Ch. Eigler
0 siblings, 1 reply; 3+ messages in thread
From: Gerald Pfeifer @ 2020-03-09 9:47 UTC (permalink / raw)
To: overseers
/home/gccadmin/scripts/update_web_docs_git is run nightly from the
gccadmin account to provide GCC's documentation on our web site.
On the new system it fails as follows:
update_web_docs_git: line 171: makeinfo: command not found
The info rpm is installed (which covers reading documentation in
.info format).
Do RHEL/CentOS also provide a makeinfo rpm?
Gerald
^ permalink raw reply [flat|nested] 3+ messages in thread
end of thread, other threads:[~2020-03-14 23:05 UTC | newest]
Thread overview: 3+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2020-03-09 9:47 gcc.gnu.org += makeinfo Gerald Pfeifer
2020-03-09 13:25 ` Frank Ch. Eigler
2020-03-14 23:05 ` Gerald Pfeifer
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).