Menu

#50 make button is inconsistently bold

workingwiki
open
5
2013-05-07
2011-02-04
Lee Worden
No

the background jobs code is supposed to change the regular make button to boldface when it inserts the background-make button, to show that it's the default. It looks like the boldface only works when there is a nonempty listing of background jobs. This may be because background.css isn't included properly otherwise. I observed this buggy behavior on yushan, don't know whether it's present on lalashan.

Discussion

Anonymous
Anonymous

Add attachments
Cancel