Skip to content

Drop spurious dependency on GAPDoc - #126

Merged
ChrisJefferson merged 1 commit into
masterfrom
mh/drop-gapdoc
Jul 29, 2026
Merged

Drop spurious dependency on GAPDoc#126
ChrisJefferson merged 1 commit into
masterfrom
mh/drop-gapdoc

Conversation

@fingolfin

Copy link
Copy Markdown
Member

No description provided.

@fingolfin

Copy link
Copy Markdown
Member Author

@ChrisJefferson assuming this passes, can you please make a new release with this in? Or just allow me to make that release

@ChrisJefferson
ChrisJefferson merged commit 807ee44 into master Jul 29, 2026
8 checks passed
@ChrisJefferson
ChrisJefferson deleted the mh/drop-gapdoc branch July 29, 2026 13:13
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