Hi there,

I was wondering why ciao_put_number_chars() in Ciao 1.10#6 is declared as

ciao_term ciao_put_number_chars(char *number_string);

and not as

ciao_term ciao_put_number_chars(const char *number_string);

I mean: ciao_put_number_chars() does not modify the parameter, does it? All the best,

Roberto