Skip to content

P145 hypocompact alias#1820

Merged
prabau merged 1 commit into
mainfrom
hypocompact
Jul 22, 2026
Merged

P145 hypocompact alias#1820
prabau merged 1 commit into
mainfrom
hypocompact

Conversation

@prabau

@prabau prabau commented Jul 22, 2026

Copy link
Copy Markdown
Collaborator

Add hypocompact as alias for P145 (strongly paracompact).

See #1783.

@prabau
prabau requested a review from Moniker1998 July 22, 2026 05:23
@prabau
prabau merged commit 9d1e85f into main Jul 22, 2026
1 check passed
@prabau
prabau deleted the hypocompact branch July 22, 2026 16:43
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants