build: config.h not installed

[jengelh]

Observed behaviour

(gap 4.10.0)
$ ./configure && make && make install DESTDIR=$PWD/rt
[...]
$ grep config.h rt/usr/local/include/gap/system.h 
*V  autoconf  . . . . . . . . . . . . . . . . . . . . . . . .  use "config.h"
#include "config.h"
22:34 a4:../gap/gap-4.10.0 > find rt -name config.h
22:34 a4:../gap/gap-4.10.0 >

As a result, extensions like curlinterface don't even build and die with

> make
  CC       src/curl_la-curl.lo
In file included from /usr/include/gap/src/gasman.h:39:0,
                 from /usr/include/gap/src/objects.h:20,
                 from /usr/include/gap/src/ariths.h:17,
                 from /usr/include/gap/src/compiled.h:17,
                 from src/curl.c:5:
/usr/include/gap/src/system.h:27:10: fatal error: config.h: No such file or directory
 #include "config.h"
          ^~~~~~~~~~

Expected behaviour

Where to start... "config.h" is a pretty bad name, it's not namespaced (and neither are the macros in it), leading to clashes left and right. It should indeed not be installed, but likewise, system.h (nor any other header file that lands in /usr/include) ought to reference it. It's something that must remain private to the build directory only.

Copy and paste GAP banner (to tell us about your setup)

[fingolfin]

You conveniently left out the part where make install prints:

	@echo "Warning, 'make install' has not yet been fully implemented"

Since multiple people seem to overlook that, I will now submit a pull request to remove make install completely (resp. replace it with an error) until the day we actually have time and resources to fully and properly implement it.

As to your other points:

• all GAP headers are installed in a GAP subdir, and thus are namespaces, i.e., you'd include them via #include <gap/HEADER.h>. There is no possible conflict with the name config.h for this reason.
• nevertheless, config.h should indeed not be installed directly as it is (that would also directly go against GNU autotools guidelines); this is one of the many reasons that make install is not finished yet.
• however, its name is not the problem.

I will close this issue now.