hol kananaskis.12-4

3 files changed, 17 insertions, 3 deletions

diff --git a/.SRCINFO b/.SRCINFO
index 5b2a6dac2b7c..2f94caae08d6 100644
--- a/.SRCINFO
+++ b/.SRCINFO
@@ -1,9 +1,9 @@
 # Generated by mksrcinfo v8
-# Mon Mar 18 12:38:15 UTC 2019
+# Mon Mar 18 12:48:26 UTC 2019
 pkgbase = hol
 	pkgdesc = HOL4 theorem-proving system
 	pkgver = kananaskis.12
-	pkgrel = 3
+	pkgrel = 4
 	url = https://hol-theorem-prover.org/
 	install = hol.install
 	arch = x86_64
diff --git a/PKGBUILD b/PKGBUILD
index c94d88d0922e..64e33178b24c 100644
--- a/PKGBUILD
+++ b/PKGBUILD
@@ -4,7 +4,7 @@
 # FIXME: holyhammer fails to build with ocaml-num
 pkgname=hol
 pkgver=kananaskis.12
-pkgrel=3
+pkgrel=4
 pkgdesc='HOL4 theorem-proving system'
 url='https://hol-theorem-prover.org/'
 arch=('x86_64')
diff --git a/hol.install b/hol.install
index 7c3bd698a968..6769d447f961 100644
--- a/hol.install
+++ b/hol.install
@@ -5,6 +5,20 @@ post_install() {
     cd /opt/hol
     poly < tools/smart-configure.sml
     bin/build --relocbuild
+
+    cat <<EOF
+*************************************************
+Emacs HOL mode
+*************************************************
+Put
+
+   (autoload 'hol "/opt/hol/tools/hol-mode"
+     "Runs a HOL session in a comint window.
+   With a numeric prefix argument, runs it niced to that level
+   or at level 10 with a bare prefix. " t)
+
+into your .emacs file
+EOF
 }
 
 post_upgrade() {