From b961030db26787fdd3ffea64a5765a028914cc5f Mon Sep 17 00:00:00 2001
From: Jon Eugster <eugster.jon@gmail.com>
Date: Fri, 12 Jul 2024 09:54:02 +0200
Subject: [PATCH] Update hints.md

---
 doc/hints.md | 1 +
 1 file changed, 1 insertion(+)

diff --git a/doc/hints.md b/doc/hints.md
index df5a1e9..87bc7d9 100644
--- a/doc/hints.md
+++ b/doc/hints.md
@@ -89,6 +89,7 @@ You can add use markdown to format your hints, for example you can use KaTex: `$
 **Escaping**: Generally, if you add text inside quotes `" "` (e.g. in `Hint`) you need to escape
 backslashes, but if you provide text inside a doc comment
 `/-- -/` (e.g. in the `Statement` description) you do not!
+Further, inside `Hint` you need to escape all opening curly brackets as `\{` since `{h}` is syntax for inserting a variable name `h`.
 
 TODO: Write a doc about latex/markdown options available.