Random change to re-trigger CI

coq · Jan 17, 2025 · 79a3b93 · 79a3b93
1 parent f5b16c7
commit 79a3b93
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/RandomChange.txt b/RandomChange.txt
@@ -0,0 +1,2 @@
+This file is used to do random changes to retrigger CI (and keep results)
+1