Skip to content

chore: README that describes server - #293

Merged
david-christiansen merged 1 commit into
masterfrom
readme-server
Aug 4, 2026
Merged

chore: README that describes server#293
david-christiansen merged 1 commit into
masterfrom
readme-server

Conversation

@david-christiansen

Copy link
Copy Markdown
Collaborator

No description provided.

@github-actions
github-actions Bot temporarily deployed to lean-lang.org/functional_programming_lean August 4, 2026 14:17 Inactive
@david-christiansen
david-christiansen merged commit 02dbbeb into master Aug 4, 2026
2 checks passed
@david-christiansen
david-christiansen deleted the readme-server branch August 4, 2026 14:17
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.

1 participant