summaryrefslogtreecommitdiffstats
path: root/divers
diff options
context:
space:
mode:
authorDavid A. Madore <david@procyon.(none)>2009-08-05 14:49:28 (GMT)
committerDavid A. Madore <david@procyon.(none)>2009-08-05 14:49:28 (GMT)
commit3f72b03eef78ca49c4fedfc3906f2fc720cde371 (patch)
treec2aa827ed71e9a7795fa488b886412a250db8504 /divers
parent81fc015d216b8a54d3b40e03a837be2f51211889 (diff)
downloadgalois-3f72b03eef78ca49c4fedfc3906f2fc720cde371.zip
galois-3f72b03eef78ca49c4fedfc3906f2fc720cde371.tar.gz
galois-3f72b03eef78ca49c4fedfc3906f2fc720cde371.tar.bz2
[tous fichiers] Suite changement '_' en '-' dans les labels (j'avais oubliƩ \refext...)
Diffstat (limited to 'divers')
-rwxr-xr-x[-rw-r--r--]divers/renommage-labels.pl2
1 files changed, 1 insertions, 1 deletions
diff --git a/divers/renommage-labels.pl b/divers/renommage-labels.pl
index 034531b..8d4d9c0 100644..100755
--- a/divers/renommage-labels.pl
+++ b/divers/renommage-labels.pl
@@ -14,6 +14,6 @@ sub changeul {
}
while (<>) {
- s/\\(label|ref)\{(.*?)\}/sprintf("\\%s{%s}",$1,changeul($2))/ge;
+ s/\\(label|ref|refext\{.*?\})\{(.*?)\}/sprintf("\\%s{%s}",$1,changeul($2))/ge;
print;
}