diff options
Diffstat (limited to 'Makefile.dev')
| -rw-r--r-- | Makefile.dev | 16 |
1 files changed, 1 insertions, 15 deletions
diff --git a/Makefile.dev b/Makefile.dev index ea1a3d40a2..68e96a57b7 100644 --- a/Makefile.dev +++ b/Makefile.dev @@ -15,7 +15,7 @@ # Debug printers in dev/ ######################### -.PHONY: devel printers camldevfiles +.PHONY: devel printers DEBUGPRINTERS:=dev/top_printers.cmo dev/vm_printers.cmo dev/checker_printers.cmo @@ -85,20 +85,6 @@ endif # But these partial targets could be quite handy for quick builds # of specific components of Coq. -########################################################################### -# OCaml dev files -########################################################################### -camldevfiles: $(MERLINFILES) META.coq - -.merlin: .merlin.in - cp -a "$<" "$@" - -%/.merlin: %/.merlin.in - cp -a "$<" "$@" - -META.coq: META.coq.in - cp -a "$<" "$@" - ############################### ### 1) general-purpose targets ############################### |