[docs] [issue18820] json.dump() ignores its 'default' option when serializing dictionary keys