diff --git a/user-doc/extract b/user-doc/extract
index 538665eca8daa4d7184281bc7e6fda09b84e4ac6..89e74825adb69c936f2203930d98f0da4a1737e7 100755
--- a/user-doc/extract
+++ b/user-doc/extract
@@ -229,5 +229,5 @@ cat $file.txt |
     /^ *@TOOLS@ *$/r      automatic/TOOLS.list
     /^ *@MODULES@ *$/r    automatic/modules.list
     /^ *@CODES@ *$/r      automatic/codes.list
-" | grep -Ev '^ *"@[A-Z]*@" *$' > ${file}PP.txt
+" | grep -Ev '^ *@[A-Z]*@ *$' > ${file}PP.txt
 done