comparison TOOLS/checktree.sh @ 35197:996cf322a88d

Mark exit_player functions as noreturn.
author reimar
date Tue, 30 Oct 2012 16:58:50 +0000
parents 92d75e703bc0
children
comparison
equal deleted inserted replaced
35196:9269e341748f 35197:996cf322a88d