2021-05-16 12:43:18 +01:00
|
|
|
#! /bin/bash
|
|
|
|
|
|
2021-06-10 22:53:56 +01:00
|
|
|
echo "Configuring MapTool"
|
|
|
|
|
|
2021-05-16 12:43:18 +01:00
|
|
|
# Scale up the GUI by 2 times for HiDPI screens
|
|
|
|
|
if [ -f "${XDG_CONFIG_HOME:-$HOME/.config}/x11/.DPI" ]; then
|
|
|
|
|
DPI="$(cat "${XDG_CONFIG_HOME:-$HOME/.config}/x11/.DPI")"
|
|
|
|
|
SCALE="$(((DPI+48)/96))"
|
2021-07-16 16:54:09 +01:00
|
|
|
doas -A sed -i "/\[JavaOptions\]/a -Dsun.java2d.uiScale=$SCALE" /opt/maptool/lib/app/MapTool.cfg
|
2021-05-16 12:43:18 +01:00
|
|
|
fi
|
