lib/scripts/feeder.pl
Fri, 04 May 2012 17:14:42 +0200 wenzelm refrain from SIGHUP handling (cf. 5f629ee2502b), which does not work on Cygwin and appears to be redundant anyway (no extra output produced within pipe);
Wed, 19 Jan 2011 21:45:50 +0100 wenzelm potentially more robust utf8 handling (cf. 3e4bb6e7c3ca);
Wed, 03 Nov 2010 21:53:56 +0100 wenzelm feeder: treat header as escaped utf8 to allow initial ML text to refer to non-ASCII file/directory names (e.g. "Documents/" on Chinese Ubuntu);
Tue, 21 Sep 2010 22:08:13 +0200 wenzelm tuned whitespace;
Sat, 20 Dec 2008 11:55:34 +0100 wenzelm removed Ids;
Mon, 21 Jun 2004 10:25:57 +0200 kleing Merged in license change from Isabelle2004
Fri, 09 Nov 2001 00:01:55 +0100 wenzelm got rid of obsolete input filtering;
Fri, 15 Sep 2000 00:16:36 +0200 wenzelm updated;
Fri, 01 Sep 2000 17:54:58 +0200 wenzelm GPLed;
Fri, 12 Feb 1999 14:40:56 +0100 oheimb renamed space2 to spacespace
Wed, 31 Dec 1997 15:17:49 +0100 wenzelm removed -i option;
Mon, 29 Dec 1997 21:39:22 +0100 wenzelm feed isabelle session;
less more (0) tip