% Extension for ciao executables in Win32
exec_ext('.cpx').
bat_ext('.bat').
