Sat, 02 Aug 2014 16:35:59 +0200 | wenzelm | more direct access to persistent blobs (see also 8953d4cc060a), avoiding fragile digest lookup from later version (which might have removed unused blobs already); | changeset | files |
Sat, 02 Aug 2014 12:24:30 +0200 | wenzelm | always resolve symlinks for local files, e.g. relevant for ML_file to load proper source via editor instead of stored file via prover; | changeset | files |
Sat, 02 Aug 2014 11:39:13 +0200 | wenzelm | tuned output; | changeset | files |
Fri, 01 Aug 2014 22:52:53 +0200 | wenzelm | prefer non-strict Execution.print, e.g relevant for redirected ML compiler reports after error (see also e79f76a48449 and 40274e4f5ebf); | changeset | files |