mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-25 04:33:45 +03:00
Cleanup after rebase
This commit is contained in:
parent
8a35a9dc74
commit
73733f03ff
2
Makefile
2
Makefile
@ -50,8 +50,8 @@ IDRIS2_BOOT_PREFIX := ${IDRIS2_CURDIR}/bootstrap-build
|
||||
|
||||
# These are the library path in the build dir to be used during build
|
||||
IDRIS2_LIBRARIES = prelude base linear network contrib test
|
||||
IDRIS2_BOOT_PATH =
|
||||
|
||||
IDRIS2_BOOT_PATH =
|
||||
$(foreach library,$(IDRIS2_LIBRARIES),$(eval IDRIS2_BOOT_PATH := $(IDRIS2_BOOT_PATH)$(IDRIS2_CURDIR)/libs/$(library)/build/ttc$(SEP)))
|
||||
export IDRIS2_BOOT_PATH := "$(IDRIS2_BOOT_PATH)"
|
||||
|
||||
|
@ -6,9 +6,6 @@ BOOTSTRAP_PREFIX=$PWD/bootstrap-build
|
||||
|
||||
IDRIS2_CG="${IDRIS2_CG-"chez"}"
|
||||
|
||||
BOOT_PATH_BASE=$IDRIS_PREFIX/idris2-$IDRIS2_VERSION
|
||||
IDRIS2_BOOT_PATH="$BOOT_PATH_BASE/prelude$SEP$BOOT_PATH_BASE/base$SEP$BOOT_PATH_BASE/linear$SEP$BOOT_PATH_BASE/network$SEP$BOOT_PATH_BASE/contrib"
|
||||
|
||||
# BOOTSTRAP_PREFIX must be the "clean" build root, without cygpath -m
|
||||
# Otherwise, we get 'git: Bad address'
|
||||
echo "$BOOTSTRAP_PREFIX"
|
||||
|
@ -15,10 +15,10 @@
|
||||
<ul class="names">
|
||||
<li><a class="code" href="prelude/index.html">prelude</a></li>
|
||||
<li><a class="code" href="base/index.html">base</a></li>
|
||||
<li><a class="code" href="contrib/index.html">contrib</a></li>
|
||||
<li><a class="code" href="network/index.html">network</a></li>
|
||||
<li><a class="code" href="test/index.html">test</a></li>
|
||||
<li><a class="code" href="linear/index.html">linear</a></li>
|
||||
<li><a class="code" href="network/index.html">network</a></li>
|
||||
<li><a class="code" href="contrib/index.html">contrib</a></li>
|
||||
<li><a class="code" href="test/index.html">test</a></li>
|
||||
</ul>
|
||||
</div>
|
||||
</body>
|
||||
|
Loading…
Reference in New Issue
Block a user