Skip to content
Snippets Groups Projects
Commit bc2c9169 authored by Björn Brandenburg's avatar Björn Brandenburg
Browse files

remove esy $HOME hack

Instead of patching the generated `Makefile.coq`, we can simply set
`$HOME` in `Makefile.coq.local`.
parent b9e54934
No related branches found
No related tags found
1 merge request!337remove Makefile patching and fix links in spec
# Prosa: include pretty documentation targets
include scripts/coqdocjs/Makefile.coqdocjs
include scripts/Makefile.alectryon
# Hack to enable esy support:
#
# In the esy container, $HOME is hidden, but this causes Coq to complain.
# We thus include a dummy $HOME value.
HOME ?= $(DESTDIR)
export HOME
--- Makefile.coq.orig 2021-10-04 11:15:22.592822933 +0200
+++ Makefile.coq 2021-10-04 11:17:18.684584261 +0200
@@ -15,6 +15,11 @@
SELF := $(lastword $(MAKEFILE_LIST))
PARENT := $(firstword $(MAKEFILE_LIST))
+# In the esy container, $HOME is hidden, but this causes Coq to complain.
+# We thus include a dummy $HOME value.
+HOME ?= $(DESTDIR)
+export HOME
+
# This file is generated by coq_makefile and contains many variable
# definitions, like the list of .v files or the path to Coq
include Makefile.conf
@@ -480,6 +485,9 @@
$(HIDE)mkdir -p html
$(HIDE)$(COQDOC) \
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment