diff options
Diffstat (limited to 'tools/testing/selftests/rcutorture/formal/srcu-cbmc/Makefile')
| -rw-r--r-- | tools/testing/selftests/rcutorture/formal/srcu-cbmc/Makefile | 17 |
1 files changed, 0 insertions, 17 deletions
diff --git a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/Makefile b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/Makefile deleted file mode 100644 index 4bed0b678f8b..000000000000 --- a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/Makefile +++ /dev/null @@ -1,17 +0,0 @@ -# SPDX-License-Identifier: GPL-2.0 -all: srcu.c store_buffering - -LINUX_SOURCE = ../../../../../.. - -modified_srcu_input = $(LINUX_SOURCE)/include/linux/srcu.h \ - $(LINUX_SOURCE)/kernel/rcu/srcu.c - -modified_srcu_output = include/linux/srcu.h srcu.c - -include/linux/srcu.h: srcu.c - -srcu.c: modify_srcu.awk Makefile $(modified_srcu_input) - awk -f modify_srcu.awk $(modified_srcu_input) $(modified_srcu_output) - -store_buffering: - @cd tests/store_buffering; make |