From 9296f9ea0adab121a5daeb8ff71612be975cf216 Mon Sep 17 00:00:00 2001 From: Marko Lindqvist Date: Tue, 10 Oct 2023 01:12:05 +0300 Subject: [PATCH 32/32] Manual: Change settings page heading to "server settings" It was talking about "server options" which contradicts our usual terminology ("server settings" & "client options") See osdn #48743 Signed-off-by: Marko Lindqvist --- tools/civmanual.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tools/civmanual.c b/tools/civmanual.c index d8fa0209e9..8b3b1667af 100644 --- a/tools/civmanual.c +++ b/tools/civmanual.c @@ -258,7 +258,7 @@ static bool manual_command(void) switch (manuals) { case MANUAL_SETTINGS: /* TRANS: markup ... Freeciv version ... markup */ - fprintf(doc, _("%sFreeciv %s server options%s\n\n"), TITLE_BEGIN, + fprintf(doc, _("%sFreeciv %s server settings%s\n\n"), TITLE_BEGIN, VERSION_STRING, TITLE_END); settings_iterate(SSET_ALL, pset) { char buf[256]; -- 2.42.0