| Fri, 05 Aug 2022 13:34:47 +0200 | wenzelm | clarified session name: treat PIDE session as Sessions.DRAFT with imports from other sessions; | changeset | files |
| Fri, 05 Aug 2022 13:23:52 +0200 | wenzelm | more robust build_hierarchy: support Resources.empty / Sessions.Structure.empty (required for Build_Job.print_log); | changeset | files |
| Thu, 04 Aug 2022 22:15:50 +0200 | wenzelm | clarified context for retrieval: more explicit types, with optional close() operation; | changeset | files |
| Thu, 04 Aug 2022 17:14:56 +0200 | wenzelm | tuned; | changeset | files |
| Thu, 04 Aug 2022 17:08:35 +0200 | wenzelm | unused; | changeset | files |
| Thu, 04 Aug 2022 14:48:05 +0200 | wenzelm | retrieve information about used files; | changeset | files |
| Thu, 04 Aug 2022 13:52:43 +0200 | wenzelm | tuned signature -- more robust; | changeset | files |