Added info option in patching script

This allows one to create information on the differences in
the various patching procedures by executing:

plumed patch -i

This information is also put into the online manual

(cherry picked from commit a273bb84d5e9e9b953eace77a2d149b0e8a13add)
Added -q option to patch

Allows to avoid verbose logging. The option is now used in user-doc/extract
to simplify the generation of code-specific notes

(cherry picked from commit 7152d46f43f7322dc9a365fceaf8c455ea85564c)

Conflicts:
	patches/patch.sh
Fixed some code-specific notes

(cherry picked from commit e1d01e84e34673c42fc149c62766570ab391c68b)
Fixed a small bug in manual generation and corrected English in code instruction pages