diff options
Diffstat (limited to '')
| -rw-r--r-- | cedilla/.gitignore | 1 | ||||
| -rwxr-xr-x | cedilla/watch | 1 |
2 files changed, 2 insertions, 0 deletions
diff --git a/cedilla/.gitignore b/cedilla/.gitignore new file mode 100644 index 0000000..7f65160 --- /dev/null +++ b/cedilla/.gitignore @@ -0,0 +1 @@ +/NEWS.text diff --git a/cedilla/watch b/cedilla/watch index f319765..b59d99b 100755 --- a/cedilla/watch +++ b/cedilla/watch @@ -1,5 +1,6 @@ #!/bin/sh +[ -f 'NEWS.text' ] && rm 'NEWS.text' wget 'http://www.pps.univ-paris-diderot.fr/~jch/software/cedilla/NEWS.text' >/dev/null 2>/dev/null if [ $? = 0 ]; then [ -f unfetchable ] && rm unfetchable |