261029.5 · 7de68afcb7256e39a2f2a0f289eb74a3a4d711eb
A repo's header names its commit by stardate, and its fetch time only after a failure
The header on the web address predated stardates and showed a short hash. It now names the commit as a version's crumbs do: the stardate, with hash and time on hover, linking that version. A commit off the main line keeps its hash. The name is read once per worktree.
The fetch time goes, since a visit fetches any copy over five minutes old and the time always read as just now. After a failed fetch the copy can be any age, so the header then shows when it was fetched and when the fetch failed.
reading declarations
Changes to doc/online-repos.md. All files
@@ -46,7 +46,9 @@ Delete the directory any time; www fetches what it needs again. A visit to a repo fetched over five minutes ago serves the cached commit at once and fetches in the background. When the branch moved, www builds the new commit's worktree beside the old one and swaps the link, so no page sees a half-updated tree. Open pages reload onto the new commit. -The header of every page in the repo names the commit shown and when it was fetched, eg `@ 52502e6 · fetched 23:40`, as a version's crumbs name a commit; the hash links the page in that commit's version, which stays put after the next fetch. When a fetch fails, the page keeps the commit it has and says the fetch failed.+The header of every page in the repo names the commit shown by its stardate, eg `@ 261029.3`, as a version's crumbs name a commit. Its hash and time show on hover. The stardate links the page in that commit's version, which stays put after the next fetch. A commit off the main line shows its hash instead.++The header gives no fetch time while fetches work, since a visit fetches any copy over five minutes old. It says `fetching` while a fetch runs. When a fetch fails, the page keeps the commit it has and says when the copy was fetched and when the fetch failed, eg `@ 261029.3 · fetched 09:12 · fetch at 17:17 failed`. A fetch takes the branches and tags. It leaves out GitHub's pull request refs, which would fill a large repo's cache with commits nobody asked for.