Skip to content

Update unison-manual.tex: the mergebatch preference has been removed. - #1197

Merged
gdt merged 2 commits into
bcpierce00:masterfrom
OnkV:patch-1
Jun 8, 2026
Merged

Update unison-manual.tex: the mergebatch preference has been removed.#1197
gdt merged 2 commits into
bcpierce00:masterfrom
OnkV:patch-1

Conversation

@OnkV

@OnkV OnkV commented Jun 6, 2026

Copy link
Copy Markdown
Contributor

Fixes a minor inconsistency in the manual.

@gdt

gdt commented Jun 6, 2026

Copy link
Copy Markdown
Collaborator

Wow, a preference removed in 2.18!

Unison contains src/strings.ml which needs frequent regeneration. How to do this is described in CONTRIBUTING.md in the Strings section. You should end up with a strings.ml commit which changes just what you are changing, but it is possible locale issues will become pesky. I'm happy to do this and add it to your commit, or you can do it if you want.

@gdt
gdt merged commit 273ec62 into bcpierce00:master Jun 8, 2026
26 checks passed
@gdt

gdt commented Jun 8, 2026

Copy link
Copy Markdown
Collaborator

Thanks for your contribution. I did the strings regen and merged it.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants