On 8/5/20 4:41 AM, Gavin Smith wrote:
On Tue, Aug 04, 2020 at 07:11:10PM -0700, Per Bothner wrote:f
--set-customization-variable js-info-dir=DIRECTORY
Good idea. I think this is the way forward. Then we can work on the various issues that you found.
Once this is in the Git repository, I'll update DomTerm to make use of it
(when configured --without-docbook). Then we can incrementally improve things.
--
--Per Bothner
[email protected] http://per.bothner.com/
