w3c / WebID

https://www.w3.org/groups/cg/webid
MIT License
14 stars 7 forks source link

Remove redundant files #34

Closed woutermont closed 7 months ago

woutermont commented 8 months ago

This PR removes some redundant files from the repo. As far as I know, these files do not contain relevant content, and they are not used by or refered to from any other file in the repo. Also keep in mind that this is a git repo, and so these files are not lost; if need be, we can easily restore them.

melvincarvalho commented 8 months ago

Good idea, thanks. They all look defunct.

jacoscaz commented 8 months ago

/chair hat off

+1 from me

jacoscaz commented 8 months ago

Any objection to this PR?

jacoscaz commented 8 months ago

Any objection to this PR? Just making sure...

jacoscaz commented 7 months ago

Thank you @woutermont !