remove `release` target as `dune-release` can be used now
This commit is contained in:
parent
4e9b9d1c66
commit
83dda5bb5d
13
Makefile
13
Makefile
|
@ -39,16 +39,3 @@ cinaps:
|
||||||
clean:
|
clean:
|
||||||
rm -rf _build *.install
|
rm -rf _build *.install
|
||||||
find . -name .merlin -delete
|
find . -name .merlin -delete
|
||||||
|
|
||||||
# This needs to be updated
|
|
||||||
.PHONY: gh-pages
|
|
||||||
gh-pages: doc
|
|
||||||
git clone `git config --get remote.origin.url` .gh-pages --reference .
|
|
||||||
git -C .gh-pages checkout --orphan gh-pages
|
|
||||||
git -C .gh-pages reset
|
|
||||||
git -C .gh-pages clean -dxf
|
|
||||||
cp -t .gh-pages/ _build/utop-api.docdir/*
|
|
||||||
git -C .gh-pages add .
|
|
||||||
git -C .gh-pages commit -m "Update Pages"
|
|
||||||
git -C .gh-pages push origin gh-pages -f
|
|
||||||
rm -rf .gh-pages
|
|
||||||
|
|
Loading…
Reference in New Issue