aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/refman
diff options
context:
space:
mode:
Diffstat (limited to 'doc/refman')
-rw-r--r--doc/refman/RefMan-uti.tex2
-rw-r--r--doc/refman/biblio.bib2
2 files changed, 2 insertions, 2 deletions
diff --git a/doc/refman/RefMan-uti.tex b/doc/refman/RefMan-uti.tex
index c282083b5..10271ce0c 100644
--- a/doc/refman/RefMan-uti.tex
+++ b/doc/refman/RefMan-uti.tex
@@ -251,7 +251,7 @@ to the \Coq\ toplevel or conversely from the \Coq\ toplevel to some
files.
{\ProofGeneral} is developed and distributed independently of the
-system \Coq. It is freely available at \verb!proofgeneral.inf.ed.ac.uk!.
+system \Coq. It is freely available at \verb!https://proofgeneral.github.io/!.
\section[Module specification]{Module specification\label{gallina}\ttindex{gallina}}
diff --git a/doc/refman/biblio.bib b/doc/refman/biblio.bib
index 70ee1f41f..e69725838 100644
--- a/doc/refman/biblio.bib
+++ b/doc/refman/biblio.bib
@@ -1199,7 +1199,7 @@ Decomposition}},
@Misc{ProofGeneral,
author = {David Aspinall},
title = {Proof General},
- note = {\url{http://proofgeneral.inf.ed.ac.uk/}}
+ note = {\url{https://proofgeneral.github.io/}}
}
@Book{CoqArt,