diff options
| author | John MacFarlane <[email protected]> | 2023-01-20 08:51:43 -0800 |
|---|---|---|
| committer | John MacFarlane <[email protected]> | 2023-01-20 08:52:36 -0800 |
| commit | e680aa18e274d422a662dc919a3cefc3c1bea505 (patch) | |
| tree | 405931308b3a9e52731caf58e0f3d90f39a866aa /linux | |
| parent | 1a4ba584e610e0d43b166ede1d791ac942057545 (diff) | |
Fix man page copying in `linux/make_artifacts.sh`.
Previously we were copying the pandoc-server.1 pandoc page to pandoc-lua.1.
This should resolve #8566, but it should be tested after a
new release candidate is generated.
Diffstat (limited to 'linux')
| -rw-r--r-- | linux/make_artifacts.sh | 12 |
1 files changed, 5 insertions, 7 deletions
diff --git a/linux/make_artifacts.sh b/linux/make_artifacts.sh index f7d76948a..d90516958 100644 --- a/linux/make_artifacts.sh +++ b/linux/make_artifacts.sh @@ -58,13 +58,11 @@ make_deb() { ln -s pandoc pandoc-server ln -s pandoc pandoc-lua cd /mnt - cp /mnt/man/pandoc.1 $DEST/share/man/man1/pandoc.1 - gzip -9 $DEST/share/man/man1/pandoc.1 - cp /mnt/man/pandoc-server.1 $DEST/share/man/man1/pandoc-server.1 - gzip -9 $DEST/share/man/man1/pandoc-server.1 - cp /mnt/man/pandoc-server.1 $DEST/share/man/man1/pandoc-lua.1 - gzip -9 $DEST/share/man/man1/pandoc-lua.1 - + for manpage in pandoc.1 pandoc-lua.1 pandoc-server.1 + do + cp /mnt/man/$manpage $DEST/share/man/man1/$manpage + gzip -9 $DEST/share/man/man1/$manpage + done cp /mnt/COPYRIGHT $COPYRIGHT echo "" >> $COPYRIGHT |