-
Notifications
You must be signed in to change notification settings - Fork 19
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Delete old unused files #228
Conversation
Pinging @tanneberger as |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
LGTM. Let's let Martin Schoeberl capture what is useful from the Patmos file. I've made a local record or the related-work file, which I do think is useful but probably doesn't belong on our website.
I can confirm these pages are not used/referenced anywhere within the website |
@cmnrd I made a backup of master. So these files don't get lost. |
Sidenote, git is created for this purpose, we can just |
That's what I did locally ;D |
@schoeberl Is it Ok to merge this? |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
From the website point of view LGTM
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I will review this and might submit a version of this as an RFC.
This deletes the
.obsolete
,.preliminary
and.less-developed
subdirectories. As far as I can see, the content of these files is quite old and not up to date. I think it is safe to delete them. Please double-check.