diff --git a/doc/infotex/exec.texi b/doc/texinfo/exec.texi
similarity index 100%
rename from doc/infotex/exec.texi
rename to doc/texinfo/exec.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
diff --git a/doc/infotex/state.texi b/doc/texinfo/state.texi
similarity index 100%
rename from doc/infotex/state.texi
rename to doc/texinfo/state.texi
diff --git a/doc/infotex/tx.texi b/doc/texinfo/tx.texi
similarity index 100%
rename from doc/infotex/tx.texi
rename to doc/texinfo/tx.texi