diff options
Diffstat (limited to 'dev/README')
| -rw-r--r-- | dev/README | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/dev/README b/dev/README index 0e40e8200..13a7343b5 100644 --- a/dev/README +++ b/dev/README @@ -41,7 +41,6 @@ go in directory and call "make" Other development tools (directory tools) ----------------------- -univdot: produces a graph of CIC universes Makefile.dir: makefile dedicated to intensive work in a given directory Makefile.subdir: makefile dedicated to intensive work in a given subdirectory Makefile.devel: utilities to automatically launch coq in various states |