Job 500

CakeML:06ed260af9472c0513a9e22e9c2af4e3a38e38a0
  Add optional timnig in ml_translatorLib [Sep 22 21:45:33]
#528 (fix-master)
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:oven2 4.13.0-37-generic x86_64 GNU/Linux

Sep 24 11:25:16 Claimed job