On Tue, Jun 2, 2020 at 10:19 AM Paul Smith wrote:
> On Tue, 2020-06-02 at 08:48 -0400, Sam Kendall wrote:
> > > I suggest that
> > > a) $HOME/.local/include is effectively added to the
> > >include_directories ...
> >
> > If two users build the same source tree, they will effectively be
> > b
On Tue, 2020-06-02 at 08:48 -0400, Sam Kendall wrote:
> > I suggest that
> > a) $HOME/.local/include is effectively added to the
> >include_directories ...
>
> If two users build the same source tree, they will effectively be
> building variants of it, each extending it with her own
> $HOME/.l
> I suggest that
> a) $HOME/.local/include is effectively added to the
>include_directories ...
If two users build the same source tree, they will effectively be building
variants of it, each extending it with her own $HOME/.local/include
directory. And if one user builds two *different* sourc
Christian Hujer (31 May 2020 15:53) wrote
> I suggest that
> a) $HOME/.local/include is effectively added to the
>include_directories, as if it were inserted in
>default_include_directories before /usr/gnu/include.
> b) Change function src/read.c/eval_makefile() to loop over
>.INCLUDE_D
Hello everyone,
I suggest that
a) $HOME/.local/include is effectively added to the include_directories, as
if it were inserted in default_include_directories before /usr/gnu/include.
b) Change function src/read.c/eval_makefile() to loop over .INCLUDE_DIRS
instead of include_directories when searc
