Differences

This shows you the differences between two versions of the page.

--- github_repositories_of_the_lab [2024/08/09 15:07] – [Saving changes as commits] 134.190.232.164
+++ github_repositories_of_the_lab [2024/08/13 11:26] (current) – [Saving changes as commits] 134.190.232.164
@@ Line 160: / Line 160: @@
 A succesfull push! If you check the online GitHub repository now in your internet browser, the file should be updated!
+You should now be familiar with the basics of interacting with a GitHub repository. Using git can be far more advanced, with different branches, re-basing etc etc but I'd say for 99% of our usecases this should suffice.
+==== Deleting a repository ====
+Deleting a local copy of your repository is as easy as removing the folder that contains the repository.
+For example
+<code>
+rm -r gospel_of_andrew
+</code>
+Easy peasy!