Am Freitag, 21. Oktober 2016 22:18:48 UTC+2 schrieb John H Palmieri: > > > > On Friday, October 21, 2016 at 12:31:01 PM UTC-7, Martin R wrote: >> >> Eli Zaretskii from the texinfo team helped me with two problems I had, >> and texinfo documentation is now almost ready to go. I need help with >> three things, which I report here, because trac is down. >> >> 1.) for some reason, it is necessary that makeinfo is called with >> "--footnote-style separate". However, Sphinx produces makefiles as defined >> by TEXINFO_MAKEFILE, see >> http://www.sphinx-doc.org/en/stable/_modules/sphinx/builders/texinfo.html >> >> What is the proper way to change that, and where should I do this? >> > > You might need to patch Sphinx for this, since it doesn't look like that > aspect of Sphinx is customizable. (So patch the linked file as part of > Sage's Sphinx package. I hope that just modifying TEXINFO_MAKEFILE to add > "--footnote-style separate" is good enough.) >
(if I have to call make myself, the following is obsolete anyway) Is this preferred over modifying TEXINFO_MAKEFILE via import sphinx.builders.texinfo sphinx.builders.texinfo.TEXINFO_MAKEFILE = ... ? (I tested that this works, why shouldn't it...) If not so, where should I put this? It looks awkward to have this in docbuild.__init__.py, but I don't know a better place. I think you should have two build targets: "sage --docbuild DOCUMENT > texinfo" which produces texinfo sources, and "sage --docbuild DOCUMENT > info" which produces the actual info files, just like the current situation > with "latex" and "pdf" output types. You would then have to deal with the > "info" case yourself: first invoke the "texinfo" builder and then run > "makeinfo" or "make" or whatever in each appropriate directory. Where are > the info files going to go? $SAGE_ROOT/local/share/info, I assume? I have no clue, but $SAGE_ROOT/local/share/info sounds reasonable. -- You received this message because you are subscribed to the Google Groups "sage-devel" group. To unsubscribe from this group and stop receiving emails from it, send an email to sage-devel+unsubscr...@googlegroups.com. To post to this group, send email to sage-devel@googlegroups.com. Visit this group at https://groups.google.com/group/sage-devel. For more options, visit https://groups.google.com/d/optout.
