| Sat, 20 Jun 2020 19:05:56 +0200 | wenzelm | tuned output; | changeset | files |
| Sat, 20 Jun 2020 16:36:32 +0200 | wenzelm | merged | changeset | files |
| Sat, 20 Jun 2020 16:18:33 +0200 | wenzelm | share cache for parallel sessions; | changeset | files |
| Sat, 20 Jun 2020 15:09:20 +0200 | wenzelm | clarified signature; | changeset | files |
| Sat, 20 Jun 2020 14:36:27 +0200 | wenzelm | more caching, notably for build/pide_session; | changeset | files |
| Sat, 20 Jun 2020 11:01:57 +0200 | wenzelm | removed pointless pide_exports: unused during "build_session" process (reverting 6a64205b491a); | changeset | files |
| Fri, 19 Jun 2020 20:15:00 +0200 | wenzelm | tuned --- avoid error in IntelliJ IDEA; | changeset | files |