##! Interface for the raw input reader. module InputRaw; export { ## Separator between input records. ## Please note that the separator has to be exactly one character long const record_separator = "\n" &redef; }