| changeset 24879 | 48e2168b0ea9 |
| parent 24875 | 8e6ca75bf5aa |
| child 24885 | 0fc7ba713a27 |
| 24878:7ed3077528b6 | 24879:48e2168b0ea9 |
|---|---|
58 |
58 |
59 SESSIONS="" |
59 SESSIONS="" |
60 for LOG in $LOGS |
60 for LOG in $LOGS |
61 do |
61 do |
62 NAME="$(basename "$LOG" .gz)" |
62 NAME="$(basename "$LOG" .gz)" |
63 if [ "$NAME" != PG -a "$NAME" != Pure ]; then |
63 if [ "$NAME" != Pure -a "$NAME" != Pure-ProofGeneral ]; then |
64 if [ -z "$SESSIONS" ]; then |
64 if [ -z "$SESSIONS" ]; then |
65 SESSIONS="$NAME" |
65 SESSIONS="$NAME" |
66 else |
66 else |
67 SESSIONS="$SESSIONS + $NAME" |
67 SESSIONS="$SESSIONS + $NAME" |
68 fi |
68 fi |