printf format specifier %i doesn't work

[GoogleCodeExporter]

The following program does not work: no numerical value is output. If I replace 
%i with %d it works. According to cplusplus.com either should work:

http://www.cplusplus.com/reference/cstdio/printf/

--------------------------------------------------
#include <stdio.h>
#include <propeller.h>

int main(){
  waitcnt(CLKFREQ + CNT);

  int myVar = 314159;
  printf("myVar: %i\n", myVar);  
  return 0;
}
--------------------------------------------------

Original issue reported on code.google.com by [email protected] on 27 Feb 2014 at 8:06