Don't commit symlinks in the repository (test-suite library_attributes)

Fix #18548 No idea why that bug happens on coqide-server and not -core or -stdlib but we have historically avoided symlinks in the git repo due to similar issues.
coq · Jan 24, 2024 · c56ab63 · c56ab63
1 parent 4335e48
commit c56ab63
Show file tree

Hide file tree

Showing 6 changed files with 3 additions and 7 deletions.
diff --git a/test-suite/Makefile b/test-suite/Makefile
@@ -346,9 +346,6 @@ unit-tests/%.ml.log: unit-tests/%.ml unit-tests/src/$(UNIT_LINK)
 # Other generic tests
 #######################################################################
 
-# There is a dependency between those two files
-prerequisite/library_attributes_require.v.log: prerequisite/library_attributes.v.log
-
 $(addsuffix .log,$(wildcard prerequisite/*.v)): %.v.log: %.v
 	@echo "TEST      $< $(call get_coq_prog_args_in_parens,"$<")"
 	$(HIDE){ \

diff --git a/test-suite/output/library_attributes_require.out b/test-suite/output/library_attributes_require.out
@@ -1,4 +1,4 @@
 File "./output/library_attributes_require.v", line 1, characters 0-37:
-Warning: Library File TestSuite.library_attributes is deprecated since XX YY.
+Warning: Library File TestSuite.deprecated_library is deprecated since XX YY.
 This library is useless.
 [deprecated-library-file-since-XX-YY,deprecated-since-XX-YY,deprecated-library-file,deprecated,default]
diff --git a/test-suite/output/library_attributes_require.v b/test-suite/output/library_attributes_require.v
@@ -1 +1 @@
-Require TestSuite.library_attributes.
+Require TestSuite.deprecated_library.
diff --git a/test-suite/prerequisite/deprecated_library.v b/test-suite/prerequisite/deprecated_library.v
@@ -0,0 +1 @@
+Attributes deprecated(note="This library is useless.", since="XX YY").
diff --git a/test-suite/prerequisite/library_attributes.v b/test-suite/prerequisite/library_attributes.v
diff --git a/test-suite/prerequisite/library_attributes_require.v b/test-suite/prerequisite/library_attributes_require.v