Skip site navigation (1)Skip section navigation (2)
Date:      Wed, 25 Sep 2024 08:33:38 GMT
From:      Yuri Victorovich <yuri@FreeBSD.org>
To:        ports-committers@FreeBSD.org, dev-commits-ports-all@FreeBSD.org, dev-commits-ports-main@FreeBSD.org
Subject:   git: 8a1be59cb545 - main - math/lean4: Remove pkg-message since both recommendations there aren't relevant any more
Message-ID:  <202409250833.48P8XcAu064176@gitrepo.freebsd.org>

next in thread | raw e-mail | index | archive | help
The branch main has been updated by yuri:

URL: https://cgit.FreeBSD.org/ports/commit/?id=8a1be59cb545963889ca0d2ec7d6da14f5da6eed

commit 8a1be59cb545963889ca0d2ec7d6da14f5da6eed
Author:     wen heping <wenheping2000@hotmail.com>
AuthorDate: 2024-09-25 04:25:24 +0000
Commit:     Yuri Victorovich <yuri@FreeBSD.org>
CommitDate: 2024-09-25 08:33:27 +0000

    math/lean4: Remove pkg-message since both recommendations there aren't relevant any more
---
 math/lean4/Makefile    | 12 ++++++++++++
 math/lean4/pkg-message | 22 ----------------------
 2 files changed, 12 insertions(+), 22 deletions(-)

diff --git a/math/lean4/Makefile b/math/lean4/Makefile
index abfc3004d07b..aa4a44690ce8 100644
--- a/math/lean4/Makefile
+++ b/math/lean4/Makefile
@@ -1,6 +1,7 @@
 PORTNAME=	lean4
 DISTVERSIONPREFIX=	v
 DISTVERSION=	4.11.0
+PORTREVISION=	1
 CATEGORIES=	math lang devel # lean4 is primarily a math theorem prover, but it is also a language and a development environment
 
 MAINTAINER=	yuri@FreeBSD.org
@@ -26,6 +27,17 @@ CXXFLAGS+=	-fPIC
 
 BINARY_ALIAS=	make=${GMAKE} python=${PYTHON_CMD}
 
+pre-everything::
+	@${ECHO_MSG} ""
+	@${ECHO_MSG} "Please note that build Lean requires /proc to be mounted."
+	@${ECHO_MSG} ""
+	@${ECHO_MSG} "  The usual way to do this is to add this line to /etc/fstab:"
+	@${ECHO_MSG} "  proc /proc procfs rw 0 0"
+	@${ECHO_MSG} ""
+	@${ECHO_MSG} "  and then run this command as root:"
+	@${ECHO_MSG} "  # mount /proc"
+	@${ECHO_MSG} ""
+
 post-install:
 	# remove empty dirs
 	@${FIND} ${STAGEDIR}${DATADIR} -type d -empty -delete
diff --git a/math/lean4/pkg-message b/math/lean4/pkg-message
deleted file mode 100644
index e0c1a26dc720..000000000000
--- a/math/lean4/pkg-message
+++ /dev/null
@@ -1,22 +0,0 @@
-[
-{ type: install
-  message: <<EOM
-================================================================================
-You installed Lean: The Theorem Prover.
-
-(1) Please note that Lean requires /proc to be mounted.
-
-    The usual way to do this is to add this line to /etc/fstab:
-    proc /proc procfs rw 0 0
-
-    and then run this command as root:
-    # mount /proc
-
-(2) You might also want to install mathlibtools (math/mathlibtools) in case
-    you need to use the mathematical library of Lean.
-    mathlibtools download this library to user's home directory for further
-    use by Lean.
-================================================================================
-EOM
-}
-]



Want to link to this message? Use this URL: <https://mail-archive.FreeBSD.org/cgi/mid.cgi?202409250833.48P8XcAu064176>