Hanspeter asked further,
| Thus as long as I quote properly is it an issue of performance?
Yes.
| It some times happens to me that I pipe twice into sed:
| | sed 'session1' | sed 'session2'
Often when people do that, one invocation of sed with the right instructions
could do both jobs -- but I've seen exceptions.
| Should I set SHELL to light version of shell (/bin/ash or /bin/sh)
| rather than something like bash?
Just guessing: as long as the lighter-weight shell can still do the job, that
sounds like a good idea.H
_______________________________________________
procmail mailing list
procmail(_at_)lists(_dot_)RWTH-Aachen(_dot_)DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/procmail