Am 19.10.2011 um 22:34 schrieb Alexander Krauss: > Does anybody know if there is a straightforward translation of the error > codes 134/137 into English?
Just Google "Unix exit codes". E.g. 134 = "The job is killed with an abort signal, and you probably got core dumped", 137 = "The job was killed because it exceeded the time limit", and 139 = "Segmentatation violation". Jasmin _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
