Typo found by Lokasz Pankowski:

dir_created -> directory_created

diff --git a/Doc/dist/dist.tex b/Doc/dist/dist.tex
index 17db70bca92c6ba80d7dba917658a5680e326e75..79471cc308444e457784b66ef00ee1db4d992ddf 100644 (file)
--- 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}