From ee0fc81f42cd510a5596f88507fcca95e710a644 Mon Sep 17 00:00:00 2001 From: Maarten Weyns Date: Sun, 24 Nov 2024 11:36:15 +0100 Subject: [PATCH] Add teamid to prints from DOMjudge --- docker/domserver/scripts/patches.d/10-default-config.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docker/domserver/scripts/patches.d/10-default-config.py b/docker/domserver/scripts/patches.d/10-default-config.py index cc582c07..bd7f5987 100755 --- a/docker/domserver/scripts/patches.d/10-default-config.py +++ b/docker/domserver/scripts/patches.d/10-default-config.py @@ -18,7 +18,7 @@ if category["category"] == "External systems": for item in category["items"]: if item["name"] == "print_command": - item["default_value"] = "/usr/bin/enscript --columns=2 --pages=-10 --landscape --pretty-print \"--header='[original]'; page $% of $=; time=$C; room='[location]'; team='[teamname]'\" [file]" + item["default_value"] = "/usr/bin/enscript --columns=2 --pages=-10 --landscape --pretty-print \"--header='[original]'; page $% of $=; time=$C; room='[location]'; team='[teamname]'; teamid='[teamid]'\" [file]" if item["name"] == "data_source": item["default_value"] = 1