[ doc ] stub

agda · Oct 28, 2015 · 4dc50dc · 4dc50dc
1 parent 5547535
commit 4dc50dc
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 1 deletion.
diff --git a/doc/user-manual/tools/command-line-options.rst b/doc/user-manual/tools/command-line-options.rst
@@ -0,0 +1,8 @@
+.. _command-line-options:
+
+********************
+Command-line options
+********************
+
+.. note::
+   This is a stub.
diff --git a/doc/user-manual/tools/index.rst b/doc/user-manual/tools/index.rst
@@ -8,9 +8,10 @@ Tools
 .. toctree::
    :maxdepth: 2
 
-   emacs-mode
    auto
+   command-line-options
    compilers
+   emacs-mode
    generating-html
    generating-latex
    package-system