From c8e1896eddfe48cab4caf58ac7fcd1a9b0a93fbf Mon Sep 17 00:00:00 2001 From: David Sancho Moreno Date: Wed, 25 Oct 2023 10:01:23 +0200 Subject: [PATCH] Add title --- website/i18n/en.json | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/website/i18n/en.json b/website/i18n/en.json index 223d96804..5ce9d30e8 100644 --- a/website/i18n/en.json +++ b/website/i18n/en.json @@ -135,13 +135,13 @@ "title": "Recursion" }, "refmt": { - "title": "refmt" + "title": "Format (refmt)" }, "regular-expression": { "title": "Regular Expression" }, "rtop": { - "title": "rtop" + "title": "REPL (rtop)" }, "string-and-char": { "title": "String & Character"