standalone: Fix output format of output_range

This commit is contained in:
David Mak 2024-07-09 13:55:48 +08:00
parent d656880e44
commit f47cdec650

View File

@ -46,10 +46,7 @@ void output_float64(double x) {
void output_range(int32_t range[3]) {
printf("range(");
if (range[0] != 0) {
printf("%d, ", range[0]);
}
printf("%d", range[1]);
printf("%d, %d", range[0], range[1]);
if (range[2] != 1) {
printf(", %d", range[2]);
}