/src/Tools/Setup/src/ default tip
drwxr-xr-x [up]
-rw-r--r-- 2025-08-03 20:34 +0100 20722 Build.java
-rw-r--r-- 2025-08-03 20:34 +0100 16103 Environment.java
-rw-r--r-- 2025-08-03 20:34 +0100 1965 Exn.java
-rw-r--r-- 2025-08-03 20:34 +0100 1214 GUI_Setup.java
-rw-r--r-- 2025-08-03 20:34 +0100 1310 Library.java
-rw-r--r-- 2025-08-03 20:34 +0100 1936 Setup.java