From 2bfd992aabda7a6dbd7db73d0ed7e7f85cd49c3e Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Thu, 28 Dec 2023 00:01:45 +0100
Subject: [PATCH] Update ProofGeneral.texi

---
 doc/ProofGeneral.texi | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index 49c1e6e46..229617fdf 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -628,7 +628,7 @@ and @ref{Advanced Script Management and Editing}.
 
 @item @i{Script editing mode}@*
 Proof General provides useful facilities for editing proof scripts,
-including syntax hilighting and a menu to jump to particular goals,
+including syntax highlighting and a menu to jump to particular goals,
 definitions, or declarations.
 Special editing functions send lines of proof script to the proof
 assistant, or undo previous proof steps.
@@ -2755,7 +2755,7 @@ text in the buffer.    This is the font that is configured by the menu
 @end example
 its customization name is @code{unicode-tokens-symbol-font-face}, but
 notice that only the font family aspect of the face is used.  Similarly,
-other fonts can be configured for controling different font families
+other fonts can be configured for controlling different font families
 (script, fraktur, etc).
 
 For symbols, good results are possible by using a proportional font for