Fixes #13353 - Add glossary to operations guide documentation#14234

sbordet merged 3 commits intojetty:jetty-12.1.xjetty/jetty.project:jetty-12.1.xfrom

afarber:13353-create-glossary-docafarber/jetty.project:13353-create-glossary-docCopy head branch name to clipboard