-
Notifications
You must be signed in to change notification settings - Fork 230
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.
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
Reverted about
, added headlines
#3387
Conversation
Actually, I'm just using |
|
For reference: (links are in orange)
|
I guess I wouldn't be opposed to changing
We have plenty of types whose afterprint is silenced, usually because either it's obvious (e.g. integers) or annoying when it shows up (e.g. we don't want a random |
26f4379
to
e30fdd5
Compare
Before this PR, the only difference between |
OK so |
Absolutely not. |
I'd say feel free to define |
correction, this was about |
I thought about that, but I actually really like how headlines about "hilbert"
locate makeDocumentTag about "hilbert" and you can switch out More practically, |
@pzinn Does this have your approval now? If so, could you submit a review? (Files Changes Tab > Green Review Changes Button) |
Here's the upshot: you can get links to documentation along with the headlines:
The output is a Table, but
help ZZ
andcode ZZ
still work.On the other hand,
about
has been reverted to it's previous format so the entries are syntax highlighted:Hopefully this is a good compromise.