diff --git a/homu/html/queue.html b/homu/html/queue.html index a28e7db..15e90f3 100644 --- a/homu/html/queue.html +++ b/homu/html/queue.html @@ -121,6 +121,43 @@ #announcement a:visited { color: #00f; } + + /* Make the rollup button vs sync button clear distinct, because sync requires some elaborate procedure. */ + button#expand-rollup { + background-color: darkcyan; + border: 2px solid #000000; + border-radius: 4px; + box-shadow: rgba(0, 0, 0, .1) 0 2px 4px 0; + box-sizing: border-box; + color: #fff; + font-size: 16px; + font-weight: 400; + padding: 10px 25px; + text-align: center; + } + + button#expand-rollup:hover { + box-shadow: rgba(0, 0, 0, .15) 0 3px 9px 0; + transform: translateY(-2px); + } + + button#synch { + background-color: red; + border: 2px solid #000000; + border-radius: 4px; + box-shadow: rgba(0, 0, 0, .1) 0 2px 4px 0; + box-sizing: border-box; + color: #fff; + font-size: 16px; + font-weight: 400; + padding: 10px 25px; + text-align: center; + } + + button#synch:hover { + box-shadow: rgba(0, 0, 0, .15) 0 3px 9px 0; + transform: translateY(-2px); + } @@ -135,6 +172,8 @@

Homu queue - {% if repo_url %}{{repo_

+

Caution: Synchronization has some caveats. Please follow the steps described in Fixing inconsistencies in the bors queue.

+

This will create a new pull request consisting of 0 PRs.

A rollup is useful for shortening the queue, but jumping the queue is unfair to older PRs who have waited too long.