Sergei Trofimov ee7734efd7 doc: agenda: add note about plugin names ...

Add a note explaining how plugin names are treated, and which names are
considered to be identical.

2018-05-14 17:08:14 +01:00

..

developers

doc: Fix code highlighting

2018-05-14 16:34:10 +01:00

users

doc: agenda: add note about plugin names

2018-05-14 17:08:14 +01:00