Tue, 17 May 2005 09:58:40 +0200 |
wenzelm |
proper treatment of directory links;
|
file |
diff |
annotate
|
Thu, 28 Apr 2005 21:36:25 +0200 |
wenzelm |
make symlink handling compatible with whitespaces
|
file |
diff |
annotate
|
Tue, 26 Apr 2005 19:49:39 +0200 |
wenzelm |
improved handling of symlinks;
|
file |
diff |
annotate
|
Mon, 21 Jun 2004 10:25:57 +0200 |
kleing |
Merged in license change from Isabelle2004
|
file |
diff |
annotate
|
Sat, 03 Feb 2001 15:21:57 +0100 |
wenzelm |
use fgrep;
|
file |
diff |
annotate
|
Thu, 30 Nov 2000 20:10:29 +0100 |
wenzelm |
/usr/bin/env bash;
|
file |
diff |
annotate
|
Wed, 22 Nov 2000 21:41:39 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Fri, 01 Sep 2000 17:47:20 +0200 |
wenzelm |
GPLed;
|
file |
diff |
annotate
|
Fri, 29 Oct 1999 12:48:27 +0200 |
wenzelm |
tuned msg;
|
file |
diff |
annotate
|
Wed, 21 May 1997 17:05:42 +0200 |
wenzelm |
fixed spelling;
|
file |
diff |
annotate
|
Tue, 22 Apr 1997 11:37:12 +0200 |
wenzelm |
removed -norc;
|
file |
diff |
annotate
|
Fri, 11 Apr 1997 17:30:15 +0200 |
wenzelm |
fixed { ... } shell syntax to accomodate bash 2.x;
|
file |
diff |
annotate
|
Tue, 11 Mar 1997 16:38:23 +0100 |
wenzelm |
tuned comments;
|
file |
diff |
annotate
|
Thu, 06 Mar 1997 12:32:58 +0100 |
wenzelm |
Oops, forgot to remove -x again;
|
file |
diff |
annotate
|
Thu, 06 Mar 1997 12:28:17 +0100 |
wenzelm |
even more robust and user friendly invocation (no longer requieres
|
file |
diff |
annotate
|