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.

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

Add emu-not-ref #176

Merged
merged 1 commit into from Mar 12, 2020
Merged

Add emu-not-ref #176

merged 1 commit into from Mar 12, 2020

Conversation

@bakkot
Copy link
Contributor

bakkot commented Mar 12, 2020

Fixes #158 by adding a new tag, emu-not-ref, which can be used to explicitly suppress auto-linking to definitions.

This tag still shows up in the HTML output, with no semantics. I feel a little bad about that but don't really want increase compile times by post-process'ing it out.

@ljharb

This comment has been minimized.

Copy link
Member

ljharb commented Mar 12, 2020

Are the build times that slow that it's an issue to remove it?

<p>An <dfn>example</dfn> is used for illustrative purposes.</p>
</div>
<div id="not-ref-section-2">
<p>When a word defined in another section (or algorithm step) is used, as in this example, it is normally automatically linked to the section containing the definition.</p>

This comment has been minimized.

Copy link
@michaelficarra

michaelficarra Mar 12, 2020

Member

Shouldn't the word "example" be auto-linked here?

This comment has been minimized.

Copy link
@bakkot

bakkot Mar 12, 2020

Author Contributor

It will be once this gets rendered! This document is written in ecmarkup.

This comment has been minimized.

Copy link
@ljharb

ljharb Mar 12, 2020

Member

:-p too bad the extension implies it's HTML

@bakkot

This comment has been minimized.

Copy link
Contributor Author

bakkot commented Mar 12, 2020

Are the build times that slow that it's an issue to remove it?

They're on the order of fifteen seconds on my reasonably nice computer, which is a length of time which feels slow to me. So, I'm going to go with yes.

Anyway, I guess we leave all the other emu- tags in. Maybe we should remove them but that can be a different PR.

@ljharb
ljharb approved these changes Mar 12, 2020
@bakkot bakkot merged commit 1cb2404 into master Mar 12, 2020
2 checks passed
2 checks passed
continuous-integration/travis-ci/pr The Travis CI build passed
Details
continuous-integration/travis-ci/push The Travis CI build passed
Details
@bakkot bakkot deleted the emu-not-ref branch Mar 12, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Linked issues

Successfully merging this pull request may close these issues.

3 participants
You can’t perform that action at this time.