Job 499

CakeML:0bca5648f09015518a7629441ff5c3e6174e3731
  Fix some things downstream of the tap changes. [Sep 20 15:16:47]
#526 (explorer)
Merging into:306e73e0ef0314393ecdbb996b50cf799375f15d
  Use Git's -C option [Sep 14 21:28:55]
HOL:5598c695d7633d13ff51408a8bcecbbb7cab7357
  Make minor tweaks to regular-play example README text [Sep 24 06:44:36]
Machine:oven1 4.15.9-300.fc27.x86_64 x86_64 GNU/Linux

Sep 24 11:23:06 Claimed job