diff --git a/user-doc/extract b/user-doc/extract index 1af0632b07948773d286ed9cadecb36e851caf0e..9dedfed57edff70d07dfccc3401eaa99d52cc3d8 100755 --- a/user-doc/extract +++ b/user-doc/extract @@ -48,7 +48,7 @@ EOF cat << EOF -\note This command line tool is implemented as a shell script. It's help message is pasted below: +\note This command line tool is implemented as a shell script. Its help message is pasted below: \verbatim EOF