# Default configuration for tilegx-linux-user