make_deb.sh: Use pandoc to create man pages.
This commit is contained in:
parent
5e10375abc
commit
e2267a8e46
1 changed files with 2 additions and 2 deletions
|
@ -44,9 +44,9 @@ mkdir -p $DEST/share/doc/pandoc-citeproc
|
|||
find $DIST -type d | xargs chmod 755
|
||||
cp $SANDBOX/bin/pandoc $DEST/bin/
|
||||
cp $SANDBOX/bin/pandoc-citeproc $DEST/bin/
|
||||
cp $MANDIR/man1/pandoc.1 $DEST/share/man/man1/
|
||||
$SANDBOX/bin/pandoc --man1 > $DEST/share/man/man1/pandoc.1
|
||||
gzip -9 $DEST/share/man/man1/pandoc.1
|
||||
cp $MANDIR/man5/pandoc_markdown.5 $DEST/share/man/man5/
|
||||
$SANDBOX/bin/pandoc --man5 > $DEST/share/man/man5/pandoc_markdown.5
|
||||
gzip -9 $DEST/share/man/man5/pandoc_markdown.5
|
||||
cp $PANDOC_CITEPROC_PATH/man/man1/pandoc-citeproc.1 $DEST/share/man/man1/
|
||||
gzip -9 $DEST/share/man/man1/pandoc-citeproc.1
|
||||
|
|
Loading…
Reference in a new issue