Skip to content

Comments

Add human-readable text to documentation of ordering_t#1859

Merged
albinahlback merged 1 commit intoflintlib:mainfrom
rburing:doc_ordering_t
Mar 20, 2024
Merged

Add human-readable text to documentation of ordering_t#1859
albinahlback merged 1 commit intoflintlib:mainfrom
rburing:doc_ordering_t

Conversation

@rburing
Copy link
Contributor

@rburing rburing commented Mar 20, 2024

Still very minimal, but contains human words.

@albinahlback albinahlback merged commit 669ab80 into flintlib:main Mar 20, 2024
@rburing rburing deleted the doc_ordering_t branch March 20, 2024 20:23
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants