diff options
| author | Maxime Dénès | 2017-12-27 10:19:21 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-12-27 10:19:21 +0100 |
| commit | 4969f9425cb0d5cd5bd735110886a0cbd2641588 (patch) | |
| tree | 6c05276df78dd476642ab5db8437e8730d19eb56 /Makefile.ide | |
| parent | 3921ff2e2c189063ec46f54cbb247570b6c59b2c (diff) | |
| parent | 5ffa147bd2fe548df3ac9053fe497d0871a5f6df (diff) | |
Merge PR #6444: [lib] Split auxiliary libraries into Coq-specific and general.
Diffstat (limited to 'Makefile.ide')
| -rw-r--r-- | Makefile.ide | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile.ide b/Makefile.ide index 7d809f67a5..08829b5544 100644 --- a/Makefile.ide +++ b/Makefile.ide @@ -41,7 +41,7 @@ IDESRCDIRS:= $(CORESRCDIRS) ide ide/utils COQIDEFLAGS=$(addprefix -I , $(IDESRCDIRS)) $(COQIDEINCLUDES) -IDEDEPS:=lib/clib.cma lib/cErrors.cmo lib/spawn.cmo +IDEDEPS:=clib/clib.cma lib/lib.cma IDECMA:=ide/ide.cma IDETOPLOOPCMA=ide/coqidetop.cma |