Merge branch 'split-options-config'
authorKim Nguyễn <kn@lri.fr>
Fri, 26 Oct 2012 12:40:15 +0000 (14:40 +0200)
committerKim Nguyễn <kn@lri.fr>
Fri, 26 Oct 2012 12:40:15 +0000 (14:40 +0200)
commit4516c5fe48693d769b62b987fe561d9aa8951695
tree9c1d4651f2d800e89506c69edd0e035747b0fdcd
parent29fa227d5418c6346167f3ec46a68bff9f104392
parent798507d52a5c11a6d852740056464241538fe76a
Merge branch 'split-options-config'

Conflicts:
src/main.ml
src/runtime.ml