Skip to content

Commit cd04e1d

Browse files
Document the Bots
Co-Authored-By: Kate Gregory <kategregory@users.noreply.github.com>
1 parent 950a177 commit cd04e1d

File tree

1 file changed

+15
-0
lines changed

1 file changed

+15
-0
lines changed

discord/index.md

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -184,6 +184,21 @@ We have also learned over time that some emojis which look fun are actually real
184184

185185
Having said that, we do add new emojis here periodically, so if there is a specific emoji you would like added, please raise it in #meta, letting us know what it means to you.
186186

187+
### Bots
188+
189+
There's @Dyno who greets people in welcome, lets you set your pronouns, and who will, on request, remind us of a few server rules.
190+
191+
And we have @npaperbot who lets you find papers for the C++ Standards Committee, also known as wg21. To use it, simply @mention the bot with a paper number or a search term.
192+
193+
Examples:
194+
195+
* `@npaperbot search "sy brand"`would search for an author name or a term like monadic
196+
* `@npaperbot p0650` returns a specific paper
197+
* In addition, if you put a paper number in square brackets, e.g. `[P0000]` or `[EWG9999]` in any sentence (even without @mentioning), it will look up the paper for you.
198+
199+
The bot doesn't have permission to run in every channel. If you have questions or comments about `@npaperbot` and the marvelous work of @Mara who has wrangled it into existence for us, please use [\#meta](https://discord.com/channels/400588936151433218/400741110936502274) for that.
200+
201+
187202
### Avoiding "Guys"
188203

189204
Many English speakers have a habit of addressing groups of people as "guys", saying things like "thanks guys" or "hello guys". While this may be intended as a gender neutral word, it doesn't feel that way to everyone. As a reminder, we have a bot, summoned by typing `!guys`, which says:

0 commit comments

Comments
 (0)