# Editor plugin user preferences