diff options
Diffstat (limited to 'FreeRTOS-Plus/Test/CBMC/patches/Makefile')
| -rw-r--r-- | FreeRTOS-Plus/Test/CBMC/patches/Makefile | 24 |
1 files changed, 24 insertions, 0 deletions
diff --git a/FreeRTOS-Plus/Test/CBMC/patches/Makefile b/FreeRTOS-Plus/Test/CBMC/patches/Makefile new file mode 100644 index 000000000..27888e63b --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/patches/Makefile @@ -0,0 +1,24 @@ +BRANCH=freertos + +PATCHED=patched + +default: + git format-patch $(BRANCH)..$(BRANCH)-cbmc-patches + +patch: + if [ ! -f $(PATCHED) ]; then \ + for p in *.patch; do \ + (cd ../../..; patch -p1 < CBMC/patches/$${p}) \ + done; \ + cat > $(PATCHED) < /dev/null; \ + fi + +unpatch: + git checkout ../../../lib + $(RM) $(PATCHED) + +#patching file lib/FreeRTOS-Plus-TCP/include/FreeRTOS_IP_Private.h +#patching file lib/include/private/list.h +#patching file lib/FreeRTOS-Plus-TCP/source/FreeRTOS_DHCP.c +#patching file lib/FreeRTOS-Plus-TCP/source/FreeRTOS_DNS.c +#patching file lib/FreeRTOS-Plus-TCP/source/FreeRTOS_TCP_WIN.c |