tuned;
authorwenzelm
Sat, 06 Oct 2007 22:07:17 +0200
changeset 24879 48e2168b0ea9
parent 24878 7ed3077528b6
child 24880 c827d25b2983
tuned;
lib/Tools/keywords
--- 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