Yes, that’s correct, and as you can see, those files have extension names .pde, not .ino, right? I suspect that maybe you have opened them in Arduino 1.0, which automatically changed the extension name to .ino.
In any case, I highly recommend you to use the VirtualBox image that I created for compiling the source code. Please follow the instructions:
http://rayshobby.net/?page_id=732#compile