diff options
| -rw-r--r-- | Doc/dist/dist.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Doc/dist/dist.tex b/Doc/dist/dist.tex index 17db70b..79471cc 100644 --- a/Doc/dist/dist.tex +++ b/Doc/dist/dist.tex @@ -1461,7 +1461,7 @@ Some functions especially useful in this context are available in the installation script. \begin{verbatim} -dir_created(pathname) +directory_created(pathname) file_created(pathname) \end{verbatim} |