Ignore page changes if we're already on that page.

This commit is contained in:
Florian Nücke 2015-04-08 19:22:00 +02:00
parent fe1cd7917b
commit 79c855d9a2

View File

@ -83,10 +83,12 @@ class Manual extends GuiScreen {
}
def pushPage(path: String): Unit = {
if (path != history.top) {
history.push(path)
scrollTo(0)
refreshPage()
}
}
def popPage(): Unit = {
if (history.size > 1) {