Remove useless opam pin (#71 & #121)

The pinning was anyways done far too late, i.e. while getting Epidisco.
hammerlab · Dec 22, 2016 · 38cd370 · 38cd370
1 parent 3432811
commit 38cd370
Showing 1 changed file with 0 additions and 2 deletions.
diff --git a/docs/disco.sh b/docs/disco.sh
@@ -168,8 +168,6 @@ cluster-status () {
 }
 
 install-epidisco () {
-    opam pin add --yes ketrew 3.0.0
-    opam reinstall ketrew --yes
     opam pin add --yes biokepi "https://github.com/hammerlab/biokepi.git"
     opam pin add --yes epidisco "https://github.com/hammerlab/epidisco.git"
 }