diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/ocamlweb-doc/Makefile | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/dev/ocamlweb-doc/Makefile b/dev/ocamlweb-doc/Makefile index 8ad226da6c..3189d7c518 100644 --- a/dev/ocamlweb-doc/Makefile +++ b/dev/ocamlweb-doc/Makefile @@ -7,7 +7,7 @@ LOCALINCLUDES=-I ../../config -I ../../tools -I ../../tools/coqdoc \ -I ../../plugins/omega -I ../../plugins/romega \ -I ../../plugins/ring -I ../../plugins/dp -I ../../plugins/setoid_ring \ -I ../../plugins/xml -I ../../plugins/extraction \ - -I ../../plugins/interface -I ../../plugins/fourier \ + -I ../../plugins/fourier \ -I ../../plugins/cc \ -I ../../plugins/funind -I ../../plugins/firstorder \ -I ../../plugins/field -I ../../plugins/subtac -I ../../plugins/rtauto \ |