diff options
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 9aa53eb2be..a091da2df7 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -3677,6 +3677,14 @@ Furthermore, you are advised not to put your own hints in the {\tt core} database, but use one or several databases specific to your development. +\subsection{\tt Remove Hints \term$_1$ \mbox{\dots} \term$_n$ :~ \ident$_1$ + \mbox{\dots} \ident$_m$} +\label{PrintHint} +\comindex{Remove Hints} + +This command removes the hints associated to terms \term$_1$ \mbox{\dots} +\term$_n$ in databases \ident$_1$ \mbox{\dots} \ident$_m$. + \subsection{\tt Print Hint} \label{PrintHint} \comindex{Print Hint} |