[Demexp-cvs] arch commit: demexp--dev--0.5--patch-63

[David]

Revision: demexp--dev--0.5--patch-63
Archive: address@hidden
Creator: David MENTRE <address@hidden>
Date: Thu Jul  7 21:13:15 CEST 2005
Standard-date: 2005-07-07 19:13:15 GMT
Renamed-files: .arch-ids/config.ml.id config/.arch-ids/config.inc.ml.id
    config.ml config/config.inc.ml
Modified-files: README config/Makefile.inc
    config/config.inc.ml configure doc/demexp-book.tex
New-patches: address@hidden/demexp--dev--0.5--patch-63
Summary: new option --for-developer in ./configure
Keywords: build

* README: document --for-developer in ./configure.

* config/config.inc.ml
  configure: 

  - new option --for-developer in ./configure. By default, production
    binaries (i.e. without autotests) are produced;

  - config.ml is now config/config.inc.ml;

  - some parts of config.ml are generated by ./configure;

  - cleanup in configure to make the script easier to understand.