Tags in the manual genre have poor behavior with spaces

Open Beginner friendly
#972 0 comments 0 reactions 0 assignees View on GitHub

Nobody has claimed this yet.

Assessment

Difficulty
2/5
Estimated time
1-3 hours
Newbie friendliness
65/100
Issue type
Bug
Clarity
Mostly clear
Activity status
Active
Domain
documentation

Research direction

Start by reproducing the failure with a section tag containing a space in the manual genre, then trace how tags are parsed and referenced. Done means spaced tags resolve correctly, or the manual clearly rejects them and references behave consistently.

Written by the indexing model from the issue text.

Description

If a section tag has a space in it, then references to it fail. Either this should work, or they should not be allowed to contain spaces.

Dominant language
Lean
Stars
384
Forks
124
Avg merge
22h 28m
Merged PRs (30d)
10

Contributor guide

No contributing guide indexed for this repository

First steps

  1. Read the whole issue, then the project's contributing guide.
  2. Comment on the issue to say you are picking it up — it saves two people doing the same work.
  3. Fork the repository and make your change on a branch.
  4. Open a pull request that references the issue number.

More from leanprover/verso

All issues in leanprover/verso

Similar issues

More Documentation issues

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.