aboutsummaryrefslogtreecommitdiffhomepage
path: root/distrib/debian/README.Debian
diff options
context:
space:
mode:
Diffstat (limited to 'distrib/debian/README.Debian')
-rw-r--r--distrib/debian/README.Debian6
1 files changed, 2 insertions, 4 deletions
diff --git a/distrib/debian/README.Debian b/distrib/debian/README.Debian
index 1aec78c0b..bb65ad197 100644
--- a/distrib/debian/README.Debian
+++ b/distrib/debian/README.Debian
@@ -20,10 +20,8 @@ bytecode version.
For interactive use of coqtop, we suggest
- either the Debian cle package
-- or the Proof-General (x)emacs mode, which unfortunately can not be
-distributed by Debian for copyright reasons. However, a Debian package
-might become available at proof general home page in the future
-(http://zermelo.dcs.ed.ac.uk/~proofgen)
+- or the Proof-General (x)emacs mode, provided in the proofgeneral-coq
+ Debian package.