Remove hints CI.

FStarLang · Jan 15, 2025 · b09c4e8 · b09c4e8
1 parent d35a5e4
commit b09c4e8
Show file tree

Hide file tree

Showing 4 changed files with 0 additions and 72 deletions.
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
@@ -11,10 +11,6 @@ defaults:
     shell: bash
 
 jobs:
-  hints: # not required
-    name: stale-hints
-    uses: ./.github/workflows/stale_hints.yml
-
   build:
     name: build
     uses: ./.github/workflows/build-ci.yml

diff --git a/.github/workflows/stale_hints.yml b/.github/workflows/stale_hints.yml
diff --git a/.scripts/check_stale_hints.sh b/.scripts/check_stale_hints.sh
diff --git a/.scripts/remove_stale_hints.sh b/.scripts/remove_stale_hints.sh