diff --git a/doc/infotex/backend.texi b/doc/texinfo/backend.texi
similarity index 100%
rename from doc/infotex/backend.texi
rename to doc/texinfo/backend.texi
diff --git a/doc/infotex/filter.texi b/doc/texinfo/filter.texi
similarity index 100%
rename from doc/infotex/filter.texi
rename to doc/texinfo/filter.texi
diff --git a/doc/infotex/index.texi b/doc/texinfo/index.texi
similarity index 100%
rename from doc/infotex/index.texi
rename to doc/texinfo/index.texi
diff --git a/doc/infotex/stack.texi b/doc/texinfo/stack.texi
similarity index 100%
rename from doc/infotex/stack.texi
rename to doc/texinfo/stack.texi