CakeML:6f71ec748c056d9a784b0d01d2b96d77b6e006ca Fix some scripts in response to changes in HOL [Jun 18 15:12:28] HOL:de873d08971c87bcfbbce86cdcd59909ef803929 Remove some Unicode in src [Jun 22 00:09:18] Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64 Jun 23 05:40:09 Claimed job Jun 23 05:40:13 Building HOL