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

The concepts macro allows linebreaks in the quoted parts of the invocation #1092

Closed
VojtechStep opened this issue Mar 22, 2024 · 0 comments · Fixed by #1093
Closed

The concepts macro allows linebreaks in the quoted parts of the invocation #1092

VojtechStep opened this issue Mar 22, 2024 · 0 comments · Fixed by #1093
Assignees
@VojtechStep
Labels
bug Something isn't working CI website

Comments

@VojtechStep
Copy link
Collaborator

E.g.

{{#concept "two
lines"}}

is accepted
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@VojtechStep VojtechStep

Labels
bug Something isn't working CI website
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Enhancements for the Concepts macro VojtechStep/agda-unimath
1 participant
@VojtechStep