From 8ae707febcd9e61ef8db7f4cd4a5a66c7f32658d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Luis=20Guzm=C3=A1n?= Date: Mon, 11 May 2026 17:08:59 -0600 Subject: [PATCH] gnome-user-docs: fix missing gnome-help. --- helpers/make-gnome-user-docs | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/helpers/make-gnome-user-docs b/helpers/make-gnome-user-docs index 2863796f..acca1535 100644 --- a/helpers/make-gnome-user-docs +++ b/helpers/make-gnome-user-docs @@ -1,6 +1,7 @@ #!/bin/sh # # Copyright (C) 2020 Rubén Rodríguez +# Copyright (C) 2026 Denis 'GNUtoo' Carikli # # This program is free software; you can redistribute it and/or modify # it under the terms of the GNU General Public License as published by @@ -17,15 +18,20 @@ # Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA 02110-1301 USA # -VERSION=2 +VERSION=3 COMPONENT=main . ./config sed '/ubuntu-docs/d' -i debian/control* + +# Ubuntu overrides all the files defined in the DO_NOT_INSTALL +# variable by deleting them. Since we don't use ubuntu-docs, we do +# want these files. +sed '/rm \$(DO_NOT_INSTALL); \\/d' -i debian/rules + touch AUTHORS changelog "Removed ubuntu-docs dependency" package -