Skip to content
Permalink
Browse files

Remove outdated script that removed all ulib hints

  • Loading branch information
s-zanella committed Nov 28, 2019
1 parent da2667a commit 148fef5df803b48b0b3282d973c55283943f7b04
Showing with 0 additions and 22 deletions.
  1. +0 −4 .docker/build/build.sh
  2. +0 −18 .scripts/git_rm_stale_hints.sh
@@ -157,10 +157,6 @@ function fetch_mitls() {
}

function refresh_fstar_hints() {
if [ -f ".scripts/git_rm_stale_hints.sh" ]; then
./.scripts/git_rm_stale_hints.sh
fi

refresh_hints "git@github.com:FStarLang/FStar.git" "git ls-files src/ocaml-output/ | xargs git add" "regenerate hints + ocaml snapshot" "."
}

This file was deleted.

0 comments on commit 148fef5

Please sign in to comment.
You can’t perform that action at this time.