diff --git a/user-doc/extract b/user-doc/extract
index 602e6202e22df0569744baf9aeb36e1659a22ed9..8e0b9e1a2a5dd69fc0c3b3bb9f2ebf14e88b66ec 100755
--- a/user-doc/extract
+++ b/user-doc/extract
@@ -34,7 +34,34 @@ do
 done
 
 # Generate all the documentation pages from comments
-cat ../*/*/*cpp |
+{
+cat ../*/*/*cpp
+# documentation for scripts:
+for file in ../scripts/*.sh
+do
+  name=$(basename ${file%.sh})
+  cat << EOF
+//+PLUMEDOC TOOLS $name
+/*
+EOF
+  ../src/lib/plumed $name --description
+
+  cat << EOF
+
+\note This command line tool is implemented as a shell script. It's help message is pasted below:
+
+\verbatim
+EOF
+  ../src/lib/plumed --no-mpi $name --help
+  cat << EOF
+\endverbatim
+*/
+//+ENDPLUMEDOC
+EOF
+
+done
+
+} |
 awk 'BEGIN{gfile="automatic/GLOSSARY.list"; dfile="automatic/DICTIONARY.list"; }{
   if($1=="//+ENDPLUMEDOC" && inside){
      inside=0;