diff options
-rw-r--r-- | packaging/ubuntu/debian/docs | 2 | ||||
-rwxr-xr-x | packaging/ubuntu/debian/rules | 2 | ||||
-rwxr-xr-x | scripts/check-version | 2 |
3 files changed, 3 insertions, 3 deletions
diff --git a/packaging/ubuntu/debian/docs b/packaging/ubuntu/debian/docs index 40dc76e3f..ea4f1cc14 100644 --- a/packaging/ubuntu/debian/docs +++ b/packaging/ubuntu/debian/docs @@ -2,6 +2,6 @@ gpl-2.0.txt README Readme.testing Readme.ubuntu -ReleaseNotes.txt +ReleaseNotes/ReleaseNotes.txt SupportedDivecomputers.txt TODO.CCR diff --git a/packaging/ubuntu/debian/rules b/packaging/ubuntu/debian/rules index 61799c31b..db893cd23 100755 --- a/packaging/ubuntu/debian/rules +++ b/packaging/ubuntu/debian/rules @@ -35,7 +35,7 @@ override_dh_auto_configure: override_dh_installchangelogs: dh_installchangelogs - dh_installchangelogs ReleaseNotes.txt + dh_installchangelogs ReleaseNotes/ReleaseNotes.txt txt2html Documentation/user-manual.txt > Documentation/user-manual.html mkdir -p debian/subsurface/usr/share/doc/subsurface cp Documentation/user-manual.txt debian/subsurface/usr/share/doc/subsurface/ diff --git a/scripts/check-version b/scripts/check-version index 24f90af79..1770ba5f4 100755 --- a/scripts/check-version +++ b/scripts/check-version @@ -15,7 +15,7 @@ set -eu #set -x # You would typically add/remove files to/from the list -files="Documentation/user-manual.txt Makefile README ReleaseNotes.txt" +files="Documentation/user-manual.txt Makefile README ReleaseNotes/ReleaseNotes.txt" whine() { echo "$0: $*" >&2 |