diff options
| author | Thomas Letan <lthms@soap.coffee> | 2020-02-23 17:38:09 +0100 |
|---|---|---|
| committer | Thomas Letan <lthms@soap.coffee> | 2020-02-23 17:38:09 +0100 |
| commit | 495b3ef6829bbd1d95320d9b922d430b405b266b (patch) | |
| tree | c2f8fe655ecd74e5306eb83c03e9d89cb90091e3 /site/cleopatra/Contents/Coq.org | |
| parent | Fix a typo in “Ltac 101” (diff) | |
Remove useless `sed' call in Coq file generation process
Diffstat (limited to 'site/cleopatra/Contents/Coq.org')
| -rw-r--r-- | site/cleopatra/Contents/Coq.org | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/site/cleopatra/Contents/Coq.org b/site/cleopatra/Contents/Coq.org index 6965927..1a73d00 100644 --- a/site/cleopatra/Contents/Coq.org +++ b/site/cleopatra/Contents/Coq.org @@ -17,7 +17,6 @@ COQDOCARG := --no-index --charset utf8 --short \ @echo " export $*.v" @coqc ${COQCARG} $< @coqdoc ${COQDOCARG} -d $(shell dirname $<) $< - @sed -i -e 's/href="$(shell basename $@)\#/href="\#/g' $@ @rm -f $(shell dirname $<)/coqdoc.css #+END_SRC |