Hi Matt,
> Plasma Strike writes:
> I am looking to add something to the install docs but I noticed there
> is the same Hyperbole manual. I assume they are generated and would
> like to know which one I should add it to. Would you prefer a diff
> or github pull request?
If you are referring to the text in "${hyperb:dir}/INSTALL:29" and
"${hyperb:dir}/man/hyperbole.texi:7567" they are close but not identical. So
they are not generated, unless Bob has some tool for this. I would expect that
it is good old copy and paste between the files.
IMHO a PR would be preferable. Much easier to collaborate that way.
%% Mats
