Allow editing a user's `external_ids` via the "Edit User" admin API. Contributed by @dklimpel.