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)
commit28e780c2b3b259a8696a44be932572b91f69583c
treef82b294db396ea85f76d28ae34d36d3b5f2ec092
parent13a15353a161600575ff4b70eda2c7a0f024d969
parentddd7804e0f846e96aa63478881ca06290cb2a39f
Merge branch 'master' into pretty-print
      New merge to add the forgotten src/config.ml