author | wenzelm |
Sat, 06 Oct 2007 22:07:17 +0200 | |
changeset 24879 | 48e2168b0ea9 |
parent 24878 | 7ed3077528b6 |
child 24880 | c827d25b2983 |
--- a/lib/Tools/keywords Sat Oct 06 22:07:16 2007 +0200 +++ b/lib/Tools/keywords Sat Oct 06 22:07:17 2007 +0200 @@ -60,7 +60,7 @@ for LOG in $LOGS do NAME="$(basename "$LOG" .gz)" - if [ "$NAME" != PG -a "$NAME" != Pure ]; then + if [ "$NAME" != Pure -a "$NAME" != Pure-ProofGeneral ]; then if [ -z "$SESSIONS" ]; then SESSIONS="$NAME" else