I'm using gcc 4.0.0 with this code:
Code:
#include <stdio.h>
#define CLOCAL 0004000
int main(int argc, char** argv) {
printf (" CLOCAL : O-%07o \n", CLOCAL);
printf (" 04000 : O-%07o \n", 04000);
return 0;
}
and I get this result:
Code:
CLOCAL : O-0004000
04000 : O-0004000
Looks like you could easily be looking at a bug there...