lib/Tools/display
Mon, 19 Sep 2011 14:40:38 +0200 wenzelm instantaneous cleanup (NB: VIEWER should be synchronous, cf. dd25b3055c4e);
Sat, 20 Dec 2008 11:39:27 +0100 wenzelm removed Ids;
Tue, 21 Oct 2008 20:18:07 +0200 wenzelm tuned usage line;
Mon, 13 Nov 2006 18:19:24 +0100 wenzelm fixed comment -- oops;
Mon, 18 Sep 2006 19:12:42 +0200 wenzelm PRIVATE_FILE: slightly more robust way to create and dispose;
Wed, 13 Apr 2005 18:48:19 +0200 wenzelm *** MESSAGE REFERS TO PREVIOUS VERSION ***
Wed, 13 Apr 2005 18:34:22 +0200 wenzelm *** empty log message ***
less more (0) -10 -7 tip