I agree with Mats. A PR is the way to go.
-- Bob
> On Jan 22, 2023, at 3:01 PM, Mats Lidell <mats.lid...@lidells.se> wrote:
>
> 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
>
