Merge branch 'dev/udpt'
commitbaf523fb7920f8f08aad37e4bb542f60f0922b85
authorygrek <ygrek@autistici.org>
Sun, 26 Sep 2010 16:21:14 +0000 (26 19:21 +0300)
committerygrek <ygrek@autistici.org>
Sun, 26 Sep 2010 16:21:14 +0000 (26 19:21 +0300)
tree47ba22ba750859e1fa034e450822451d3513a0f6
parentaa32f5f6ae62c9f2d08b8ca5c45225586107a59b
parentcc516fcf0aa112975ea1e18b984444c6fbe977cf
Merge branch 'dev/udpt'

Conflicts:

config/Makefile.config.in
config/Makefile.in
config/configure.in
src/utils/bitstring/bitstring.ml.in
src/utils/bitstring/bitstring.mli
src/utils/bitstring/bitstring_c.c
src/utils/bitstring/bitstring_persistent.mlc4
src/utils/bitstring/bitstring_persistent.mli
src/utils/bitstring/pa_bitstring.mlt
config/configure.in