Hi,
I am trying to compile example from 'Download' tutorial under Cygwin.
http://sel4.systems/Download/

What I get is:

[KERNEL]
 [BF_GEN] arch/object/structures_gen.h
 [BF_GEN] plat/machine/hardware_gen.h
 [BF_GEN] api/types_gen.h
 [CPP] src/arch/ia32/machine_asm.s
 [AS] src/arch/ia32/machine_asm.o
/home/user/seL4test/kernel/src/arch/ia32/machine_asm.S: Assembler messages:
/home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:15: Warning: .type pseudo-op used outside of .def/.endef ignored.
/home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:15: Error: junk at end of line, first unrecognized character is `o'
/home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:20: Warning: .size pseudo-op used outside of .def/.endef ignored.
/home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:20: Error: junk at end of line, first unrecognized character is `o'
/home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:22: Warning: .type pseudo-op used outside of .def/.endef ignored.
/home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:22: Error: junk at end of line, first unrecognized character is `i'
/home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:26: Warning: .size pseudo-op used outside of .def/.endef ignored.
/home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:26: Error: junk at end of line, first unrecognized character is `i'
/home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:30: Warning: .type pseudo-op used outside of .def/.endef ignored.
/home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:30: Error: junk at end of line, first unrecognized character is `i'
/home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:34: Warning: .size pseudo-op used outside of .def/.endef ignored.
/home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:34: Error: junk at end of line, first unrecognized character is `i'
/home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:36: Warning: .type pseudo-op used outside of .def/.endef ignored.
/home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:36: Error: junk at end of line, first unrecognized character is `i'
/home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:41: Warning: .size pseudo-op used outside of .def/.endef ignored.
/home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:41: Error: junk at end of line, first unrecognized character is `i'
/home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:43: Warning: .type pseudo-op used outside of .def/.endef ignored.
/home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:43: Error: junk at end of line, first unrecognized character is `i'
/home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:49: Warning: .size pseudo-op used outside of .def/.endef ignored.
/home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:49: Error: junk at end of line, first unrecognized character is `i'
..........


What to do with it?