diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-09 18:40:14 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-09 18:40:14 +0200 |
| commit | ba50753e9da60a23a40dedea59fb7f25e3ba4d15 (patch) | |
| tree | 826df6950995c06af6a9dabc5dffee96285c938c | |
| parent | 8770f0db6e16aaff27a14fd48eed2ae70338f3df (diff) | |
No need anymore for referring to xml directory in MLINCLUDES.
| -rw-r--r-- | Makefile.common | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile.common b/Makefile.common index 6dc193d6e..b47a3e322 100644 --- a/Makefile.common +++ b/Makefile.common @@ -67,7 +67,7 @@ CORESRCDIRS:=\ PLUGINS:=\ omega romega micromega quote \ - setoid_ring xml extraction fourier \ + setoid_ring extraction fourier \ cc funind firstorder Derive \ rtauto nsatz syntax decl_mode btauto |