Skip to content
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

Remove a file that's no longer used. #612

Open
wants to merge 1 commit into
base: master
Choose a base branch
from

Conversation

bangerth
Copy link
Member

@tjhei says that publications.include is no longer used, though I have not been able to find how script.sh in @tjhei's docker image actually looks these days. Either way, if that's how it is, let's nuke the file to make sure we don't actually think that it needs to be kept up to date.

@tjhei
Copy link
Member

tjhei commented Nov 26, 2024

Agreed that we should clean this up.

But I am worried that this will break the CI workflow as the original .html used on the old website is still generated.

@bangerth
Copy link
Member Author

@tjhei Where does that happen? The file is not referenced anywhere in this repository, so it must be in a different repository. I suspect it's this line, right?

docker run --rm -v "$(PWD)/temp:/home/bob/source" tjhei/dealii-java-jabref

I just can't seem to find the script that this repo runs (script.sh).

@tjhei
Copy link
Member

tjhei commented Nov 28, 2024

I will take care of it in the next few days.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants