Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

create/update doc/ref/user_pref_list.xml automatically #5681

Merged
merged 2 commits into from
Mar 18, 2024
Merged

create/update doc/ref/user_pref_list.xml automatically #5681

merged 2 commits into from
Mar 18, 2024

Conversation

ThomasBreuer
Copy link
Contributor

resolves #5680

@ThomasBreuer ThomasBreuer added kind: bug Issues describing general bugs, and PRs fixing them topic: documentation Issues and PRs related to documentation topic: tests issues or PRs related to tests release notes: not needed PRs introducing changes that are wholly irrelevant to the release notes labels Mar 18, 2024
@ThomasBreuer
change the strategy ...
3808cd5 
Apparently there are several places in the code where the
documentation gets processed.
Thus there is now `UpdateXMLForUserPreferences`,
which gets called in `doc/make_doc.in` and in `tst/extractmanuals.g`.
@fingolfin fingolfin merged commit 203cc91 into gap-system:master Mar 18, 2024
25 checks passed
@ThomasBreuer ThomasBreuer deleted the TB_user_pref_list branch March 20, 2024 10:43
fingolfin pushed a commit that referenced this pull request May 6, 2024
@ThomasBreuer @fingolfin
create/update doc/ref/user_pref_list.xml automatically (#5681)
8afcc3c
Feyorsh added a commit to Feyorsh/nixpkgs that referenced this pull request Jul 15, 2024
@Feyorsh
gap: 4.12.2 -> 4.13.0
a4de74a 
Bumped to fix compilation errors on Clang 16; an outstanding issue
with `userpref` tests is fixed in
gap-system/gap#5681, but a patch cannot be
fetched naively because the GAP tarball and Git repo are not the
same (no .gitignore in tarball).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@fingolfin fingolfin fingolfin approved these changes

Assignees
No one assigned
Labels
backport-to-4.13-DONE kind: bug Issues describing general bugs, and PRs fixing them release notes: not needed PRs introducing changes that are wholly irrelevant to the release notes topic: documentation Issues and PRs related to documentation topic: tests issues or PRs related to tests
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

Userpref test failure
2 participants
@ThomasBreuer @fingolfin