[GRASS-git] [OSGeo/grass] 7d99ee: wxGUI/preferences: allow the user to change the fo...

[Tomas Zigo]

  Branch: refs/heads/main
  Home:   https://github.com/OSGeo/grass
  Commit: 7d99ee393b28917b2d0d33dfbb2adf58ae001ef4
      https://github.com/OSGeo/grass/commit/7d99ee393b28917b2d0d33dfbb2adf58ae001ef4
  Author: Tomas Zigo <50632337+tmszi at users.noreply.github.com>
  Date:   2023-12-08 (Fri, 08 Dec 2023)

  Changed paths:
    M gui/wxpython/core/settings.py
    M gui/wxpython/gui_core/ghelp.py
    M gui/wxpython/gui_core/preferences.py

  Log Message:
  -----------
  wxGUI/preferences: allow the user to change the font size/face of the manual page (#3291)