--segv-nospin is now default.
authorMorgan Deters <mdeters@cs.nyu.edu>
Tue, 13 Aug 2013 15:59:26 +0000 (11:59 -0400)
committerMorgan Deters <mdeters@cs.nyu.edu>
Tue, 13 Aug 2013 23:26:29 +0000 (19:26 -0400)
commitc957465176d46a7f06a96393619db5e6f4fbda38
treee90b8e26072f2ef91c3f1b1572287dd3ddc88c39
parent1af67a61059009407dd9833b126581d2c5e5c662
--segv-nospin is now default.
src/main/driver_unified.cpp
src/main/main.h
src/main/options
src/main/util.cpp
src/options/base_options