Skip to content

Commit

Permalink
add type-in-type flag
Browse files Browse the repository at this point in the history
  • Loading branch information
benediktahrens committed Aug 13, 2024
1 parent 039a6bc commit c3d8b57
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -57,7 +57,7 @@ include build/CoqMakefile.make
endif
everything: all html install
OTHERFLAGS += $(MOREFLAGS)
OTHERFLAGS += -noinit -indices-matter -w none
OTHERFLAGS += -noinit -indices-matter -type-in-type -w none
ifeq ($(VERBOSE),yes)
OTHERFLAGS += -verbose
endif
Expand Down

0 comments on commit c3d8b57

Please sign in to comment.