lib/scripts/feeder.pl
2012-05-04 wenzelm 2012-05-04 refrain from SIGHUP handling (cf. 5f629ee2502b), which does not work on Cygwin and appears to be redundant anyway (no extra output produced within pipe);
2011-01-19 wenzelm 2011-01-19 potentially more robust utf8 handling (cf. 3e4bb6e7c3ca);
2010-11-03 wenzelm 2010-11-03 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);
2010-09-21 wenzelm 2010-09-21 tuned whitespace;
2008-12-20 wenzelm 2008-12-20 removed Ids;
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2001-11-09 wenzelm 2001-11-09 got rid of obsolete input filtering;
2000-09-15 wenzelm 2000-09-15 updated;
2000-09-01 wenzelm 2000-09-01 GPLed; more robust handling of spaces in args / file names;
1999-02-12 oheimb 1999-02-12 renamed space2 to spacespace
1997-12-31 wenzelm 1997-12-31 removed -i option;
1997-12-29 wenzelm 1997-12-29 feed isabelle session;