File tree 1 file changed +2
-2
lines changed
1 file changed +2
-2
lines changed Original file line number Diff line number Diff line change @@ -628,7 +628,7 @@ and @ref{Advanced Script Management and Editing}.
628
628
629
629
@item @i {Script editing mode }@*
630
630
Proof General provides useful facilities for editing proof scripts,
631
- including syntax hilighting and a menu to jump to particular goals,
631
+ including syntax highlighting and a menu to jump to particular goals,
632
632
definitions, or declarations.
633
633
Special editing functions send lines of proof script to the proof
634
634
assistant, or undo previous proof steps.
@@ -2755,7 +2755,7 @@ text in the buffer. This is the font that is configured by the menu
2755
2755
@end example
2756
2756
its customization name is @code {unicode-tokens-symbol-font-face }, but
2757
2757
notice that only the font family aspect of the face is used. Similarly,
2758
- other fonts can be configured for controling different font families
2758
+ other fonts can be configured for controlling different font families
2759
2759
(script, fraktur, etc).
2760
2760
2761
2761
For symbols, good results are possible by using a proportional font for
You can’t perform that action at this time.
0 commit comments