• MARCHE Claude's avatar
    better association of goals when checksums and shapes cannot be read · 0226395a
    MARCHE Claude authored
    new goals are associated to old goals directly in the order they appear.
    they are all marked obsolete, unless the theory itself is found non
    obsolete (thanks to the new checksums for theories)
    in other words, reloading a session on a file that did not change results
    in non-obsolete goals, even if checksums and shapes are absent (e.g. if
    the file was not put under version control)
session_scheduler.ml 33.8 KB