EXTRA: server/extensions.py (no longer generated)
