Anton Shestakov <av6@dwimlabs.net>, Sat, 08 May 2021 07:52:45 +0800
terminalrc: add new terminal options, switch to 11 font (the same as old 10?)
BackgroundDarkness=0,800000
BackgroundMode=TERMINAL_BACKGROUND_TRANSPARENT
ColorPalette=#000000;#cc0000;#4e9a06;#c4a000;#3465a4;#75507b;#06989a;#d3d7cf;#555753;#ef2929;#8ae234;#fce94f;#739fcf;#ad7fa8;#34e2e2;#eeeeec
MiscCursorShape=TERMINAL_CURSOR_SHAPE_BLOCK
MiscDefaultGeometry=80x24
MiscInheritGeometry=FALSE
MiscMiddleClickOpensUri=FALSE
MiscSearchDialogOpacity=100
MiscShowRelaunchDialog=TRUE
MiscShowUnsafePasteDialog=TRUE
MiscTabCloseMiddleClick=TRUE
MiscTabPosition=GTK_POS_TOP
MiscUseShiftArrowsToScroll=FALSE
ScrollingBar=TERMINAL_SCROLLBAR_NONE
TitleMode=TERMINAL_TITLE_REPLACE