[07:34:03] <p858snake|cloud>	 Jhs: was it a recent addition, iirc cs needs to be restarted to start the indexing process
[07:53:01] <Jhs>	 p858snake|cloud, seems it was added in October, so I would've expected an indexing to happen already: https://gerrit.wikimedia.org/r/plugins/gitiles/labs/codesearch/+/e0ce8589697c97856672edfabcb58ed2dea1126f%5E%21/write_config.py (but maybe that change hasn't been deployed yet?)
[09:29:30] <p858snake|cloud>	 Jhs: looks like that might not be needed anymore and should do every 24hr https://www.mediawiki.org/wiki/Codesearch/Admin
[22:58:07] <gry>	 is there an android app for mediawiki that, if the wiki has notifications installed, delivers them as push notifications?