search

UniFormal / MMT

The MMT Language and System
https://uniformal.github.io/
Other
68 stars 22 forks source link

mmt make alltex should not include _region_.tex #542

Closed kohlhase closed 3 years ago

kohlhase commented 3 years ago

There are a couple of files that should not be included in the generated all.tex, I now find 

\begin{center} \LARGE File: \url{_region_.tex} \end{center}
\input{_region_} \newpage

and the _region_.tex is something emacs creates. It would be nice to exclude that.

lambdaTotoro commented 3 years ago

Currently the inputs are based on all the files that are present in the directory. I can definitely include _region_.tex in a list of files that are explicitly to be excluded, but I don't think there's a general pattern on which files to in/exclude by name, correct?

kohlhase commented 3 years ago

that is correct. The only general pattern I can suggest ist that we only want to have the files there that are added in git.

kohlhase commented 3 years ago

that allows us to use the .gitignore to mark files as non-essential (and we have to do that in any case).

lambdaTotoro commented 3 years ago

After some (very) rudimentary glob to regex conversion, this is done as of commit 1a3b1ce06209802f49fd7727ae73272612eb78aa. The code considers not just the one .gitignore, but all that can be found from the local directory all the way up to the archive root.

I tested it on my machine with the AI repository, and it works fine. Let me know if you need it tweaked or if problems pop up.

kohlhase commented 3 years ago

very nice, thanks a lot. Actually I had been hoping that there is a git API command that tells you about ignored files, that you could have used (instead of partially re-implementing). Indeed there seems to be: https://git-scm.com/docs/git-check-ignore

kohlhase commented 3 years ago

I should probably have hinted at that in the issue description.

lambdaTotoro commented 3 years ago

Ah, I have been out-git-fu'd. :D But an elegant one-liner is of course better than a 50-LOC hack. Commit 8bbc160af8379ea2b9d13b93b6d85323eabea92c now has the call to git check-ignore instead.

kohlhase commented 3 years ago

very nice, works for me.