summaryrefslogtreecommitdiff
path: root/riscv
diff options
context:
space:
mode:
Diffstat (limited to 'riscv')
-rw-r--r--riscv/Makefile1
1 files changed, 1 insertions, 0 deletions
diff --git a/riscv/Makefile b/riscv/Makefile
index 52bc150b..5ac7597f 100644
--- a/riscv/Makefile
+++ b/riscv/Makefile
@@ -29,6 +29,7 @@ Riscv.thy: riscv.lem riscv_extras.lem
riscv_extras.lem \
riscv_types.lem \
riscv.lem
+ sed -i 's/datatype ast/datatype (plugins only: size) ast/' Riscv_types.thy
riscv.lem: $(SAIL_SRCS)
$(SAIL_DIR)/sail -lem -o riscv -lem_mwords -lem_lib Riscv_extras $^