Job 2519

CakeML:c61ffae7522febb39764768caec3eb99d9af977c
  Avoid storing decode_encode twice [Aug 02 16:37:11]
#1032 (new-double-ffi)
Merging into:cfaaf93a40910a30ef16b5d3c5ece7d68e97daa2
  Merge pull request #1033 from CakeML/fix-translator-pair-type [Aug 01 15:02:04]
HOL:718d989039b65d4ab82e8b979876c68c04869da1
  Implement general Quote syntax [Jul 26 07:07:20]
Machine:stove 5.15.0-86-generic x86_64 GNU/Linux

Aug 02 19:33:45 Claimed job
Aug 02 19:33:47 Reusing HOL