diff options
Diffstat (limited to 'debian/coq.dirs.in')
-rw-r--r-- | debian/coq.dirs.in | 7 |
1 files changed, 0 insertions, 7 deletions
diff --git a/debian/coq.dirs.in b/debian/coq.dirs.in deleted file mode 100644 index 5c2ef467..00000000 --- a/debian/coq.dirs.in +++ /dev/null @@ -1,7 +0,0 @@ -usr/bin -usr/lib/coq/contrib/micromega -usr/share/coq -usr/share/man/man1 -usr/share/pixmaps -usr/share/texmf/tex/latex/misc -@OCamlDllDir@ |