From 83dda5bb5dba67af153e848224209557c5f15ef3 Mon Sep 17 00:00:00 2001 From: Anil Madhavapeddy Date: Thu, 31 Jan 2019 10:31:59 +0000 Subject: [PATCH] remove `release` target as `dune-release` can be used now --- Makefile | 13 ------------- 1 file changed, 13 deletions(-) diff --git a/Makefile b/Makefile index 93b4f0c..e2e7cc7 100644 --- a/Makefile +++ b/Makefile @@ -39,16 +39,3 @@ cinaps: clean: rm -rf _build *.install 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