+ public void font_size_changed(int font_size) {
+ if (map != null)
+ map.font_size_changed(font_size);
+ if (statsTable != null)
+ statsTable.font_size_changed(font_size);
+ }
+
+ public void units_changed(boolean imperial_units) {
+ if (map != null)
+ map.units_changed(imperial_units);
+ if (enable != null)
+ enable.units_changed(imperial_units);
+ }
+