Adjust size of GUI elements and theme - Githubissues

Dynamic-Book / drgeo

GNU Dr. Geo, a Dynamic Knowledge Model on geometry

https://www.gnu.org/s/dr-geo

GNU General Public License v3.0

18 stars 1 forks source link

Adjust size of GUI elements and theme #28

Closed hilaire closed 6 months ago

hilaire commented 6 months ago

The DrGeo world menu, should come with new entries :

to adjust size of GUI elements
to select Bright/Dark theme