diff options
Diffstat (limited to 'libs/minisat/00_UPDATE.sh')
-rw-r--r-- | libs/minisat/00_UPDATE.sh | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/libs/minisat/00_UPDATE.sh b/libs/minisat/00_UPDATE.sh index eb278c307..2ffc11553 100644 --- a/libs/minisat/00_UPDATE.sh +++ b/libs/minisat/00_UPDATE.sh @@ -15,4 +15,5 @@ sed -i -e '1 i #define __STDC_FORMAT_MACROS' *.cc patch -p0 < 00_PATCH_mkLit_default_arg.patch patch -p0 < 00_PATCH_remove_zlib.patch patch -p0 < 00_PATCH_no_fpu_control.patch +patch -p0 < 00_PATCH_typofixes.patch |