Wiki

Clone wiki

inf225public / make-glossary

#! /bin/sh

git rm -rf glossary || rm -rf glossary mkdir -p glossary

DIR=pwd

cd $HOME/git/slebook/inf225/glossary

IFS=?

for f in ; do sed -e 's/\lowercase {([^}])}/\1/g' \ -e 's/\T1\textendash/–/g' -e 's/\T1\textemdash/—/g' \ -e 's/\T1\textquoteleft /‘/g' \ -e 's/\T1\textquoteright /’/g' \ -e 's/\T1\textquotedblleft /“/g' \ -e 's/\T1\textquotedblright /”/g' \ -e 's/\⟨/〈/g' -e 's/\⟩/〉/g' \ -e 's/\discretionary {-}{}{}//g' \ -e 's/\in /∈ /g' \ -e 's/\epsilon /ε/g' \ -e 's/\(protect|relax) //g' \ -e 's/\$\rightarrow \$/→/g' \ -e 's/\epsilon /ε/g' \ -e 's/\ /\ /g' \ -e 's/\$/*/g' \ -e 's/\&overline;a/ā/g' \ -e 's/\&underdot;n/ṇ/g' \ < "$f" > "$DIR/glossary/$f" done

cd "$DIR" git add glossary

Updated