HomeIsabelle/Phabricator

Unlink any existing statistics file. Open will fail if it exists. Report an…

Description

Unlink any existing statistics file. Open will fail if it exists. Report an error if --exportstats
is given but we can't create the statistics.

Details

Provenance
dcjmAuthored on Aug 6 2020, 1:15 PM
Parents
rPOLYML4c21a9d8e5e7: Small change to 8e4d341 to allow compilation when int is IntInf.int.
Branches
Unknown
Tags
Unknown