Skip to content
This repository has been archived by the owner on Oct 14, 2023. It is now read-only.

Online tutorial's links do not support Cmd-click, do not preserve browser history, and more #519

Closed
carlpaten opened this issue Mar 30, 2015 · 4 comments

Comments

@carlpaten
Copy link

I'm listing several bugs here, but they all have the same root cause and fix, related to how internal links are handled.

Bug #1: from https://leanprover.github.io/tutorial/index.html, I click the drop-down list and select "02 Dependent Type Theory". The URL address does not meaningfully change; if I send the address to someone and they open it, it brings them to chapter 1.

Expected behaviour: if I am on the chapter 2 page, the URL should be a permalink to chapter 2.

Bug #2: if I go further down this page, there is a link to the chapter on type classes. Cmd-click (OS X) creates a new tab with the chapter in question, but the current page also moves to the type classes chapter.

Expected behaviour: Cmd-click should have the same effect as right-click -> open in new tab.

Note: this is probably reproducible on Windows with Ctrl-click.

Bug #3: after opening one internal link, all other internal links appear purple, as if visited.

Expected behaviour: only links to chapters which I've actually visited should appear purple.

@soonhokong
Copy link
Contributor

@LilRed, could you open the issue at https://github.com/leanprover/tutorial/issues/new?

@carlpaten
Copy link
Author

Certainly - sorry for the bother.

@soonhokong
Copy link
Contributor

Thank you!

@carlpaten
Copy link
Author

Moved to leanprover/tutorial#76.

Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants