| changeset 35022 | c844b93dd147 |
| parent 33684 | 29d8aaeb56e5 |
| child 52439 | 4cf3f6153eb8 |
| 35021:c839a4c670c6 | 35022:c844b93dd147 |
|---|---|
64 cat "$LOG" |
64 cat "$LOG" |
65 else |
65 else |
66 gzip -dc "$LOG" |
66 gzip -dc "$LOG" |
67 fi |
67 fi |
68 echo |
68 echo |
69 done | \ |
69 done | "$ISABELLE_HOME/lib/scripts/keywords" "$KEYWORDS_NAME" "$SESSIONS" |
70 perl -w "$ISABELLE_HOME/lib/scripts/keywords.pl" "$KEYWORDS_NAME" "$SESSIONS" |