[ docs ] Remove user manual back to it's own folder.

It seems that this actually still works on readthedocs.org.
agda · Oct 13, 2015 · 2bb4b8a · 2bb4b8a · phile314 · Oct 13, 2015
1 parent 0188c95
commit 2bb4b8a
Show file tree

Hide file tree

Showing 7 changed files with 0 additions and 0 deletions.
diff --git a/doc/.gitignore → doc/user-manual/.gitignore b/doc/.gitignore → doc/user-manual/.gitignore
diff --git a/doc/Makefile → doc/user-manual/Makefile b/doc/Makefile → doc/user-manual/Makefile
diff --git a/doc/conf.py → doc/user-manual/conf.py b/doc/conf.py → doc/user-manual/conf.py
diff --git a/doc/index.rst → doc/user-manual/index.rst b/doc/index.rst → doc/user-manual/index.rst
diff --git a/doc/license.rst → doc/user-manual/license.rst b/doc/license.rst → doc/user-manual/license.rst
diff --git a/doc/make.bat → doc/user-manual/make.bat b/doc/make.bat → doc/user-manual/make.bat
diff --git a/doc/reflection.rst → doc/user-manual/reflection.rst b/doc/reflection.rst → doc/user-manual/reflection.rst