Admin/mira.py
Thu, 09 Apr 2015 22:56:31 +0200 wenzelm obsolete;
Mon, 14 Jul 2014 15:39:23 +0200 noschinl mira.py: building jEdit plugin is required for makeall
Thu, 05 Jun 2014 14:37:44 +0200 noschinl mira: USER_HOME must exist for building JEdit documentation
Wed, 04 Jun 2014 15:32:25 +0200 noschinl set USER_HOME to affect also ISABELLE_PATH et al
Mon, 16 Sep 2013 12:51:33 +0200 wenzelm updated to smlnj 110.76;
Thu, 20 Dec 2012 09:49:00 +0100 noschinl tuned "use build timeout": tuples cannot be concatenated
Wed, 19 Dec 2012 16:41:55 +0100 krauss use build timeout (wall clock time, default: 2h)
less more (0) -30 -10 -7 tip