Rename the placeholder file from .gitkeep to PLACEHOLDER

`dune` does not recognize `.gitkeep` as a file, so `glob_files_rec ../case-studies/*` would file because the directory `case-studies` appears empty. This `./case-studies/PLACEHOLDER` file may be deleted once a test case is added to the repository.
Beluga-lang · Jan 27, 2024 · 5b58972 · 5b58972
1 parent 52cb6b1
commit 5b58972
Showing 1 changed file with 0 additions and 0 deletions.
diff --git a/case-studies/.gitkeep → case-studies/PLACEHOLDER b/case-studies/.gitkeep → case-studies/PLACEHOLDER