Fri, 13 Jun 2025 15:18:16 +0200 | wenzelm | more robust GUI setup via Java, instead of shell script; | file | diff | annotate |
Tue, 06 May 2025 17:03:56 +0200 | wenzelm | tuned comments; | file | diff | annotate |
Wed, 27 Mar 2024 17:11:46 +0100 | wenzelm | support for "all" platforms; | file | diff | annotate |