Merge branch 'refs/heads/t/doc-improvements'
authorAndre Noll <maan@tuebingen.mpg.de>
Sun, 26 Mar 2017 16:04:52 +0000 (18:04 +0200)
committerAndre Noll <maan@tuebingen.mpg.de>
Sun, 26 Mar 2017 16:04:52 +0000 (18:04 +0200)
commit2e24b91148dda8ea52b308a4b5e0ef08c0f11267
treec5c424c35b36412a9fd538d47758614933c9d74c
parent11ef904f216bc07351a88381755b6a34b90d1ef5
parent5fa12abdb75ead7fa6995d38047e10a579df250e
Merge branch 'refs/heads/t/doc-improvements'

Another topic branch that was cooking for far too long.

* refs/heads/t/doc-improvements:
  Switch from grutatxt to markdown.
  INSTALL: Link to the gengetopt web page.
  manual: Fix a whitespace issue.
  manual: Add example for interactive mode.
  manual: Add two more examples.
  manual: Add example query for omitting a directory.
  manual: Add short option example.
  manual: Remove pointless "time" prefix.
  manual: Improve documentation of --output.
Makefile