diff options
author | 2015-03-10 21:11:43 -0400 | |
---|---|---|
committer | 2015-03-10 21:11:43 -0400 | |
commit | c29d132351cbb720d8bb0b5edfb72813e4fa51d4 (patch) | |
tree | d6139d04d25348e2ecca3ce533a5017bbf99211d /debian/urweb-doc.doc-base | |
parent | 7a0c076d19966bb8f9ea3bfa30ad5d1b15a1c9d2 (diff) |
Create doc package
Diffstat (limited to 'debian/urweb-doc.doc-base')
-rw-r--r-- | debian/urweb-doc.doc-base | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/debian/urweb-doc.doc-base b/debian/urweb-doc.doc-base new file mode 100644 index 00000000..d4676ed4 --- /dev/null +++ b/debian/urweb-doc.doc-base @@ -0,0 +1,7 @@ +Document: urweb-manual +Title: The Ur/Web Manual +Author: Adam Chlipala +Section: Programming/UrWeb + +Format: PDF +Files: /usr/share/doc/urweb/manual.pdf.gz
\ No newline at end of file |