Merge pull request #3680 from FStarLang/_nik_no_hints

Removing hints from the repo
FStarLang · Jan 15, 2025 · 7cd7efc · 7cd7efc
2 parents b9200e3 + b09c4e8
commit 7cd7efc
Show file tree

Hide file tree

Showing 2,124 changed files with 67 additions and 545,989 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