Admin/page/DISTNAME
author kleing
Thu, 20 Jun 2002 21:44:54 +0200
changeset 13230 c5fad3c40d45
parent 9954 734e0ec40f44
child 15809 3355abbeced1
permissions -rw-r--r--
fail more gracefully, return proper exit codes, allow preset DISTPREFIX

Isabelle-internal