Merge commit 'dd35d451'

* commit 'dd35d451':
  doc: Change wrong term to avoid confusion

Conflicts:
	doc/developer.texi

No change, as the wrong term is not part of our docs
Merged-by: Michael Niedermayer <michaelni@gmx.at>