diff --git a/Makefile.in b/Makefile.in
index b3533dbda783bae32673f24c6bc8db7d6611a0ff..965378b40d32dbd6e7dfe53e4ad9d1523d85ab81 100644
--- a/Makefile.in
+++ b/Makefile.in
@@ -81,7 +81,7 @@ EXTCMXA = $(addsuffix .cmxa,$(EXTLIBS))
 
 all: @OCAMLBEST@
 
-.PHONY: byte opt clean depend all
+.PHONY: byte opt clean depend all install
 
 #############
 # Why library
@@ -199,6 +199,10 @@ clean::
 	rm -f src/main.cm[iox] src/main.annot src/main.o
 	rm -f bin/why.byte bin/why.opt
 
+install::
+	mkdir -p $(BINDIR)
+	cp -f bin/why.@OCAMLBEST@ $(BINDIR)/why3
+
 ########
 # Whyml
 ########
@@ -475,9 +479,14 @@ bin/why3-cpulimit: src/tools/@CPULIMIT@.c
 clean::
 	rm -f bin/why3-cpulimit src/tools/*~
 
+install::
+	mkdir -p $(BINDIR)
+	cp -f bin/why3-cpulimit $(BINDIR)
+
 #########
 # drivers
 #########
+
 #Only generated drivers
 DIR_DRIVERS := drivers/
 
@@ -557,6 +566,12 @@ testl-type: bin/whyml.byte
 # installation
 ###############
 
+install::
+	mkdir -p $(LIBDIR)/why3
+	cp -f --parents theories/*.why theories/*/*.why $(LIBDIR)/why3/
+	cp -f --parents drivers/*.drv $(LIBDIR)/why3/
+	cp -f why.conf $(LIBDIR)/why3/
+
 ## install: install-binary install-lib install-man
 ##
 ## BINARYFILES = $(BINARY) bin/why-ide.$(OCAMLBEST)
@@ -856,9 +871,12 @@ headers:
 Makefile: Makefile.in config.status
 	./config.status --file $@
 
-src/config.ml: src/config.ml.in config.status
+src/config.sh: src/config.sh.in config.status
 	./config.status --file $@
 
+src/config.ml: src/config.sh config.status
+	LIBDIR=$(LIBDIR) src/config.sh
+
 doc/version.tex: doc/version.tex.in config.status
 	./config.status --file $@
 
diff --git a/configure.in b/configure.in
index 09da4070c52614fa8b3fbf2f97521500efeb61a5..d72004d329b388b9479f30d49bcf532a91adff6d 100644
--- a/configure.in
+++ b/configure.in
@@ -336,9 +336,10 @@ dnl AC_SUBST(PDFVIEWER)
 
 # Finally create the Makefile from Makefile.in
 dnl AC_OUTPUT(Makefile)
-AC_CONFIG_FILES(Makefile src/config.ml doc/version.tex)
+AC_CONFIG_FILES(Makefile src/config.sh doc/version.tex)
 AC_OUTPUT
-chmod a-w Makefile src/config.ml doc/version.tex
+chmod a-w Makefile src/config.sh doc/version.tex
+chmod a+x src/config.sh
 
 # Summary
 
diff --git a/src/config.ml.in b/src/config.ml.in
deleted file mode 100644
index 536ce105dfbd8257862658d20088db92f8bb99f0..0000000000000000000000000000000000000000
--- a/src/config.ml.in
+++ /dev/null
@@ -1,37 +0,0 @@
-(**************************************************************************)
-(*                                                                        *)
-(*  Copyright (C) 2010-                                                   *)
-(*    Francois Bobot                                                      *)
-(*    Jean-Christophe Filliatre                                           *)
-(*    Johannes Kanig                                                      *)
-(*    Andrei Paskevich                                                    *)
-(*                                                                        *)
-(*  This software is free software; you can redistribute it and/or        *)
-(*  modify it under the terms of the GNU Library General Public           *)
-(*  License version 2.1, with the special exception on linking            *)
-(*  described in file LICENSE.                                            *)
-(*                                                                        *)
-(*  This software is distributed in the hope that it will be useful,      *)
-(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
-(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-# 21 "src/config.ml.in"
-
-let why_version   = "@VERSION@"
-let why_builddate = "@BUILDDATE@"
-let why_plugins   = ("@enable_plugins@" = "yes")
-
-module Dynlink_ = struct
-  let is_native = true
-  let loadfile_private _ = assert false
-
-  type error
-  exception Error of error
-  let error_message _ = (assert false : string)
-end
-
-module Dynlink = struct
-  include @DYNLINK@
-end
diff --git a/src/config.sh.in b/src/config.sh.in
new file mode 100644
index 0000000000000000000000000000000000000000..2fffb39cbf280bd8af9e9794efecfda4bc585dc2
--- /dev/null
+++ b/src/config.sh.in
@@ -0,0 +1,22 @@
+
+F=src/config.ml
+
+echo "let why_version   = \"@VERSION@\"" > $F
+echo "let why_builddate = \"@BUILDDATE@\"" >> $F
+echo "let why_plugins   = (\"@enable_plugins@\" = \"yes\")" >> $F
+echo "let why_libdir    = \"$LIBDIR/why3\"" >> $F
+
+echo "
+module Dynlink_ = struct
+  let is_native = true
+  let loadfile_private _ = assert false
+
+  type error
+  exception Error of error
+  let error_message _ = (assert false : string)
+end
+
+module Dynlink = struct
+  include @DYNLINK@
+end
+" >> $F