Job 477

CakeML:ba6cd57cd66a00ef98c1c6f06bbeb9e6e760f1c9
  Use Git's -C option [Sep 12 09:51:12]
#524 (build-info)
Merging into:66a35311787bb43f72e8e758209a4745f288cdfe
  Fix a bug in PrettyPrinter.fromWord64 [Sep 12 17:03:31]
HOL:7323105f50960bdec1b33c513576e5d1d313b62f
  Document match_term when vars with same names have different types [Sep 12 05:39:17]
Machine:cakeml1794 4.4.0-98-generic x86_64 GNU/Linux

Sep 13 01:55:18 Claimed job
Sep 13 01:55:28 Building HOL
Sep 13 01:55:37 FAILED: building HOL