> On 9 Apr 2018, at 20:25, Frank Heckenbach <[email protected]> wrote: > > Hans Åberg wrote: > >>> So, try this: >>> >>> cd /usr/share/bison >>> sudo patch < /path/to/extra-header-prefix.diff >>> cd /your/source/dir >>> rm -f stack.hh position.hh location.hh >>> make clean >>> make >> >> I wouldn't do that for two reasons: screwing up the installation, >> and security reasons - > > Alright, do "patch --dry-run" before actually patching. > >> one should do the changes while not root, and copy them to the >> installation location. > > Well, then: > > - make a copy of /usr/share/bison > - patch the copy > - as root, copy changed files back
Already did this - you were too quick in the reply. :-)
