change main file

fpvandoorn · Apr 12, 2024 · 076d9b8 · 076d9b8
1 parent 6a7d93e
commit 076d9b8
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/BonnAnalysis.lean b/BonnAnalysis.lean
@@ -1 +1,2 @@
-def hello := "world"
+-- When adding a new file, import it in this file
+import BonnAnalysis.Plancherel