From 43585ac89e7068a259aecf185cc74f17e195a0bd Mon Sep 17 00:00:00 2001 From: Nathan McCarty Date: Mon, 20 Jan 2025 21:54:54 -0500 Subject: [PATCH] Move idris projects to right place --- {Idris => projects/Idris}/.gitignore | 0 {Idris => projects/Idris}/Idris.ipkg | 0 {Idris => projects/Idris}/pack.toml | 0 {Idris => projects/Idris}/src/Idris.idr | 0 {Idris => projects/Idris}/src/Posts/HelloWorld.md | 0 5 files changed, 0 insertions(+), 0 deletions(-) rename {Idris => projects/Idris}/.gitignore (100%) rename {Idris => projects/Idris}/Idris.ipkg (100%) rename {Idris => projects/Idris}/pack.toml (100%) rename {Idris => projects/Idris}/src/Idris.idr (100%) rename {Idris => projects/Idris}/src/Posts/HelloWorld.md (100%) diff --git a/Idris/.gitignore b/projects/Idris/.gitignore similarity index 100% rename from Idris/.gitignore rename to projects/Idris/.gitignore diff --git a/Idris/Idris.ipkg b/projects/Idris/Idris.ipkg similarity index 100% rename from Idris/Idris.ipkg rename to projects/Idris/Idris.ipkg diff --git a/Idris/pack.toml b/projects/Idris/pack.toml similarity index 100% rename from Idris/pack.toml rename to projects/Idris/pack.toml diff --git a/Idris/src/Idris.idr b/projects/Idris/src/Idris.idr similarity index 100% rename from Idris/src/Idris.idr rename to projects/Idris/src/Idris.idr diff --git a/Idris/src/Posts/HelloWorld.md b/projects/Idris/src/Posts/HelloWorld.md similarity index 100% rename from Idris/src/Posts/HelloWorld.md rename to projects/Idris/src/Posts/HelloWorld.md