equal
deleted
inserted
replaced
14 { |
14 { |
15 echo |
15 echo |
16 echo "Usage: $PRG [OPTIONS]" |
16 echo "Usage: $PRG [OPTIONS]" |
17 echo |
17 echo |
18 echo " Options are:" |
18 echo " Options are:" |
19 echo " -h TEXT head text" |
19 echo " -h TEXT head text (encoded as utf8)" |
20 echo " -p emit my pid" |
20 echo " -p emit my pid" |
21 echo " -q do not pipe stdin" |
21 echo " -q do not pipe stdin" |
22 echo " -t TEXT tail text" |
22 echo " -t TEXT tail text" |
23 echo |
23 echo |
24 echo " Output texts (pid, head, stdin, tail), then wait to be terminated." |
24 echo " Output texts (pid, head, stdin, tail), then wait to be terminated." |