theme: Add optional argument to REPLAY_THEME for the benefit of user-defined themes

See #4184
This commit is contained in:
josteph 2019-08-10 14:08:19 +00:00 committed by jostephd
parent ed7d60ce1b
commit 08352d2ab4

View file

@ -400,13 +400,15 @@
[/report_countdown]
#enddef
#define REPLAY_THEME FONT_SMALL_SIZE
#arg LEFT_MARGIN
=#endarg
[replay]
[add]
[panel]
id=replay-panel
image=themes/editor/classic/toolbar.png
ref=top-panel
rect="=,+0,+842,+41"
rect="{LEFT_MARGIN},+0,842,+41"
xanchor=left
yanchor=fixed
[/panel]
@ -414,7 +416,7 @@
[change]
id=main-map
ref=top-panel
rect="=,+41,+842,768"
rect="{LEFT_MARGIN},+41,842,768"
[/change]
[add]
[action]