Re: [Monetdb-developers] [Monetdb-checkins] MonetDB5/src/tools monetdb.mx, , 1.19, 1.20