diff options
| author | Arnold D. Robbins <arnold@skeeve.com> | 2019-04-14 19:13:29 +0300 |
|---|---|---|
| committer | Arnold D. Robbins <arnold@skeeve.com> | 2019-04-14 19:13:29 +0300 |
| commit | c67cff427d7a0628786cac067f3d55e53892e5c8 (patch) | |
| tree | 318da297ae3bd7e3049813a20329a086b8214b58 | |
| parent | 07b29f7ca515fb4c3c762133c6b7a159c92a9091 (diff) | |
| parent | ee3d30930741e566f5a1fee4831bba004048ae9a (diff) | |
| download | egawk-c67cff427d7a0628786cac067f3d55e53892e5c8.tar.gz egawk-c67cff427d7a0628786cac067f3d55e53892e5c8.tar.bz2 egawk-c67cff427d7a0628786cac067f3d55e53892e5c8.zip | |
Merge branch 'gawk-5.0-stable' of ssh://git.sv.gnu.org/srv/git/gawk into gawk-5.0-stable
| -rw-r--r-- | pc/ChangeLog | 5 | ||||
| -rw-r--r-- | pc/Makefile | 2 |
2 files changed, 7 insertions, 0 deletions
diff --git a/pc/ChangeLog b/pc/ChangeLog index 862c2b87..ca9d80e3 100644 --- a/pc/ChangeLog +++ b/pc/ChangeLog @@ -1,3 +1,8 @@ +2019-04-13 Eli Zaretskii <eliz@gnu.org> + + * Makefile (install1): Copy the *.txt files needed to display the + manuals in the stand-alone Info reader. + 2019-04-12 Arnold D. Robbins <arnold@skeeve.com> * ChangeLog.1: Rotated ChangeLog into this file. diff --git a/pc/Makefile b/pc/Makefile index 85594a65..d15ff10f 100644 --- a/pc/Makefile +++ b/pc/Makefile @@ -335,6 +335,8 @@ install1: cp doc/*.1 $(prefix)/share/man/man1 cp doc/*.info $(prefix)/share/info cp doc/*.png $(prefix)/share/info + cp doc/*.txt $(prefix)/share/info + rm -f $(prefix)/share/info/awkforai.txt # install2 is equivalent to install1, but doesn't require cp, sed, etc. install2: |