Mark H Weaver m...@netris.org skribis:
Federico Beffa be...@ieee.org writes:
From 06441ea6992808ef96139ab171269172dc65f2db Mon Sep 17 00:00:00 2001
From: Federico Beffa be...@fbengineering.ch
Date: Sun, 5 Apr 2015 21:59:18 +0200
Subject: [PATCH] build-system/gnu: Add 'delete-info-dir-file'
On Sat, Mar 28, 2015 at 3:37 PM, Ludovic Courtès l...@gnu.org wrote:
Federico Beffa be...@ieee.org skribis:
given that the file .../share/info/dir creates clashes in user
profiles and that it is anyway handled with the help of info-dir
substitutes, shouldn't we systematically delete them with
Federico Beffa be...@ieee.org writes:
From 06441ea6992808ef96139ab171269172dc65f2db Mon Sep 17 00:00:00 2001
From: Federico Beffa be...@fbengineering.ch
Date: Sun, 5 Apr 2015 21:59:18 +0200
Subject: [PATCH] build-system/gnu: Add 'delete-info-dir-file' phase.
*
Federico Beffa be...@ieee.org skribis:
given that the file .../share/info/dir creates clashes in user
profiles and that it is anyway handled with the help of info-dir
substitutes, shouldn't we systematically delete them with the help,
e.g., of a phase in gnu-build-system?
We should do that,
Hi,
given that the file .../share/info/dir creates clashes in user
profiles and that it is anyway handled with the help of info-dir
substitutes, shouldn't we systematically delete them with the help,
e.g., of a phase in gnu-build-system?
Regards,
Fede
