[Demexp-dev] Troublesome build system modifications

[GISQUET Christophe]

Good evening

I find the current way of modifying the build process a bit bothersome. First 
you have to edit Makefile to test, then port changes to config/Makefile.inc

Therefore I propose that Makefile simply includes config/Makefile.inc, hoping 
it is not a gnu-ism. This *greatly* reduces the complexity in testing and 
porting changes. Anyway, I don't think that many platforms would be affected 
if it were the case. Furthermore, this begs the question whether 
config/Makefile.inc should simply become Makefile, including Makefile.inc 
generated by configure. This sounds somewhat more logical and the way used by 
almost all software I know.

Last but not least, it may be interesting to:
- have Makefile be generated on a configure change; storing the options passed 
to configure could be used when reinvoking it
- a change in Makefile would cause a recompilation
I believe that this is overkill (recompiling automatically when developer 
knows best when he should recompile), but I still wanted to mention it.

Best regards,
--
Christophe GISQUET

diff -r bffa766612ce configure
--- a/configure Sun Sep 24 12:09:31 2006 +0200
+++ b/configure Mon Sep 25 21:33:45 2006 +0200
@@ -474,8 +474,8 @@ fi
 
 echo ".PHONY: default" >> Makefile
 echo "default: $default" >> Makefile
-
-cat Makefile.inc >> Makefile
+echo "include config/Makefile.inc" >> Makefile
+#cat Makefile.inc >> Makefile
 
 # produce config.ml