diff options
| author | Juan Marin Noguera <juan@mnpi.eu> | 2023-06-14 19:43:50 +0200 |
|---|---|---|
| committer | Juan Marin Noguera <juan@mnpi.eu> | 2023-06-14 19:43:50 +0200 |
| commit | 57d209473984c176ab416501e30526e98ca6045b (patch) | |
| tree | 3667d77d6a004ee6bceb0c3cae38100a9c5608a5 /.gitignore | |
| parent | efa19f8660bca027b977a57db0e5f35bdec643a4 (diff) | |
Concepto de mónada
Diffstat (limited to '.gitignore')
| -rw-r--r-- | .gitignore | 3 |
1 files changed, 2 insertions, 1 deletions
@@ -13,4 +13,5 @@ auto/ *~ _region_.tex prv_*.fmt -*.prv
\ No newline at end of file +*.prv +*.out
\ No newline at end of file |