Re: Where do I add stuff to the Hyperbole manual?

[Robert Weiner]

I agree with Mats.  A PR is the way to go.

-- Bob

> On Jan 22, 2023, at 3:01 PM, Mats Lidell <mats.lidell@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
>