Merge branch 'master' into pretty-print
authorKim Nguyễn <kn@lri.fr>
Sun, 21 Oct 2012 07:54:08 +0000 (09:54 +0200)
committerKim Nguyễn <kn@lri.fr>
Sun, 21 Oct 2012 07:54:08 +0000 (09:54 +0200)
      New merge to add the forgotten src/config.ml


Trivial merge