mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-25 04:33:45 +03:00
Do not install papers
library
This commit is contained in:
parent
dccb80d0bf
commit
502aa6f4fc
2
Makefile
2
Makefile
@ -244,14 +244,12 @@ install-libdocs: libdocs
|
||||
mkdir -p ${PREFIX}/${NAME_VERSION}/docs/network
|
||||
mkdir -p ${PREFIX}/${NAME_VERSION}/docs/test
|
||||
mkdir -p ${PREFIX}/${NAME_VERSION}/docs/linear
|
||||
mkdir -p ${PREFIX}/${NAME_VERSION}/docs/papers
|
||||
cp -r libs/prelude/build/docs/* ${PREFIX}/${NAME_VERSION}/docs/prelude
|
||||
cp -r libs/base/build/docs/* ${PREFIX}/${NAME_VERSION}/docs/base
|
||||
cp -r libs/contrib/build/docs/* ${PREFIX}/${NAME_VERSION}/docs/contrib
|
||||
cp -r libs/network/build/docs/* ${PREFIX}/${NAME_VERSION}/docs/network
|
||||
cp -r libs/test/build/docs/* ${PREFIX}/${NAME_VERSION}/docs/test
|
||||
cp -r libs/linear/build/docs/* ${PREFIX}/${NAME_VERSION}/docs/linear
|
||||
cp -r libs/papers/build/docs/* ${PREFIX}/${NAME_VERSION}/docs/papers
|
||||
install -m 644 support/docs/* ${PREFIX}/${NAME_VERSION}/docs
|
||||
|
||||
|
||||
|
@ -19,7 +19,6 @@
|
||||
<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="papers/index.html">papers</a></li>
|
||||
</ul>
|
||||
</div>
|
||||
</body>
|
||||
|
Loading…
Reference in New Issue
Block a user