2013/7/3 Bastien <b...@gnu.org>: > Hi Sebastian, > > Sebastian Wiesner <lunary...@gmail.com> writes: > >> Hardly the answer I hoped to get. > > Please let us know the answer you hoped to get, it will > surely help us giving it :)
Uh, I hoped for a “easy, just toggle that customize setting” sort of answer, not the “well, write it yourself” one ;) More precisely I had hoped for an easy way to plug Texinfo's HTML Xref Configuration [1] into Org, which would have given proper HTML links for free. I'll put Org mode migration of said manual on hold, for I currently lack the time to write a proper link exporter myself. I might get back to it later, and look into the details of Texinfo's system, but I can't promise anything. I'll probably just stick to Texinfo, until someone else does the dirty work ;) Anyway, thank you for your answer, and please excuse the rather harsh brevity of my previous answer. Sebastian Wiesner [1]: http://www.gnu.org/software/texinfo/manual/texinfo/html_node/HTML-Xref-Configuration.html#HTML-Xref-Configuration