From af797811ded1477404df59ae43346b1e52176fdb Mon Sep 17 00:00:00 2001 From: jorts Date: Wed, 6 Aug 2025 18:24:08 +0100 Subject: [PATCH] make buttons work better --- docs/assets/extra.js | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/docs/assets/extra.js b/docs/assets/extra.js index 1553a44..6bbc4ac 100644 --- a/docs/assets/extra.js +++ b/docs/assets/extra.js @@ -431,20 +431,20 @@ function createSourcePaneHeader() { const links = document.createElement('div'); links.className = 'source-pane-links'; - // Original button - const originalBtn = document.createElement('a'); - originalBtn.className = 'source-control-btn source-control-original'; - originalBtn.target = '_blank'; - originalBtn.innerHTML = 'original'; - // Archive button const archiveBtn = document.createElement('a'); archiveBtn.className = 'source-control-btn source-control-archive'; archiveBtn.target = '_blank'; - archiveBtn.innerHTML = 'archive'; + archiveBtn.innerHTML = 'Open this archive copy'; + + // Original button + const originalBtn = document.createElement('a'); + originalBtn.className = 'source-control-btn source-control-original'; + originalBtn.target = '_blank'; + originalBtn.innerHTML = 'View original'; - links.appendChild(originalBtn); links.appendChild(archiveBtn); + links.appendChild(originalBtn); // Right side - close button only const controls = document.createElement('div');