Admin/page/DISTNAME
author kleing
Fri, 27 May 2005 01:09:44 +0200
changeset 16095 f6af6b265d20
parent 15809 3355abbeced1
permissions -rw-r--r--
put global isatest settings in one file, sourced by the other scripts

Isabelle2004