update main!

[CeresBarros]

It's time :P

@achubaty, I've removed development from teh GHA workflow, because it keeps creating html/md files that conflict with the main branch on every push during a PR.

Perhaps this is not ideal, but the manual is not a true test either and it gets rebuild on push to main anyways (when PR is merged)

[achubaty]

Hmm, I don't think that's a good workflow. Those are super easy conflicts to resolve: take the devel version of those files.

If main is regularly updated AND the documentation is kept up to date during devel (and tested locally!), it may not make a real practical difference... but we know that devel docs aren't regularly maintained, and if they aren't built locally and problems fixed, then we won't see issues for weeks/months until the next merge to main.

[CeresBarros]

take the devel version of those files.

Sure. It's just that I found my self doing that like 10 times today, lol. And what was happening was, if I took the devel versions there would be "nothing to merge" and the conflict would't be "resolved".
How are you dealing with that?

[achubaty]

You can also rebuild the docs locally and use the new files (taking neither the main nor devel versions).

[CeresBarros]

I don't think that doesn't work either because (assuming there's a PR devl -> main)

1. you render/build locally on devel
2. you commit and push
3. GHA is triggered and builds the files again
4. the conflict between devel and main wrt those files is still there and reported in the PR

[CeresBarros]

The "only" way I found to "remove" the conflict was to:
locally merge main -> devel, take at least one of the files (e.g. the HTML) and push that merged commit to devel, then accept PR. But I think eventually, once GHA rebuilds the HTML on devel, the conflict comes back if the PR is not merged beforehand