# HG changeset patch # User Oleksandr Gavenko # Date 1546165308 -7200 # Node ID 0dba496629c95ab9932d16566be4a0fe59b58335 # Parent 56099ea766772e63f2e98b189c3f928990f023b8 Allow to override font size by local settings. diff -r 56099ea76677 -r 0dba496629c9 .hgignore --- a/.hgignore Thu Dec 20 00:47:02 2018 +0200 +++ b/.hgignore Sun Dec 30 12:21:48 2018 +0200 @@ -3,6 +3,8 @@ # or at Windows 'cmd': # bash# cmd /c assoc .cmd | { IFS='=' read ext name; echo $name; [ -z $name ] || cmd /c ftype $name; } +Makefile.cfg.override + syntax: glob *.a *.elc diff -r 56099ea76677 -r 0dba496629c9 .minttyrc --- a/.minttyrc Thu Dec 20 00:47:02 2018 +0200 +++ b/.minttyrc Sun Dec 30 12:21:48 2018 +0200 @@ -44,7 +44,8 @@ # Nice looks and support large amount of chars. Font=Courier New BoldAsFont=yes -FontHeight=12 +# 10 on low DPI, 12 on hi DPI +FontHeight=@CFG_FONT_SIZE@ AllowBlinking=no FontSmoothing=None diff -r 56099ea76677 -r 0dba496629c9 Makefile --- a/Makefile Thu Dec 20 00:47:02 2018 +0200 +++ b/Makefile Sun Dec 30 12:21:48 2018 +0200 @@ -17,6 +17,16 @@ .DEFAULT_GOAL = help ################################################################ +# Config. + +CFG_FILE := Makefile.cfg +include $(CFG_FILE) + +# Override defaults. +CFG_LOCAL_FILE := Makefile.cfg.override +-include $(CFG_LOCAL_FILE) + +################################################################ # Platform definition. ifeq '' '$(HOME)' @@ -51,7 +61,7 @@ OVERRIDDEN_ITEMS := \ .fvwm .xxkbrc .xmodmaprc .stalonetrayrc \ - .inputrc .minttyrc .Xdefaults .xinitrc .xserverrc .screenrc \ + .inputrc .Xdefaults .xinitrc .xserverrc .screenrc \ .dircolors .colordiffrc \ .env .bashrc .bash_completion .bash_completion.d .zshrc .vimrc .ssh \ .pylintrc .pystartup .tclshrc .npmrc .guile \ @@ -171,6 +181,7 @@ endif mkdir -p $(HOME)/.local/share/applications/ $(INSTALL_DATA) .local/share/applications/mimeapps.list $(HOME)/.local/share/applications/ + sed -e 's=@CFG_FONT_SIZE@=$(CFG_FONT_SIZE)=' <.minttyrc >$(HOME)/.minttyrc .PHONY: uninstall uninstall: diff -r 56099ea76677 -r 0dba496629c9 Makefile.cfg --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Makefile.cfg Sun Dec 30 12:21:48 2018 +0200 @@ -0,0 +1,6 @@ +# 7x13 on low DPI, 7x14 on hi DPI. +CFG_FONT_NAME := 7x14 +# 10 on low DPI, 12 on hi DPI. +CFG_FONT_SIZE := 12 +CFG_COLS := 160 +CFG_ROWS := 40