fixed all

This commit is contained in:
2018-05-18 10:26:58 +02:00
parent 91aaecdb73
commit 04afe9b44a
3 changed files with 17 additions and 18 deletions
+16 -17
View File
@@ -1,25 +1,24 @@
<?php
if (count($argv)==1) die("no file\n");
array_shift($argv);
foreach($argv as $i => $value) {
if ($i == 0) continue;
if(!file_exists($value)) die("no file ".$value."\n");
if (count($argv)==0) die("no file\n");
foreach($argv as $value) {
if(!file_exists($value)) die("no file ".$value."\n");
}
foreach($argv as $i => $value) {
if ($i == 0) continue;
echo "Cleaning $value\n";
$content = file_get_contents($value);
$pat = '/(\\\\(?:label|cref|Cref|ref))\\{([^}]+)\\}/';
$fixed = preg_replace_callback($pat, function($match) {
return $match[1] . '{' . trim(str_replace('-', '_', $match[2])) . '}';
}, $content);
file_put_contents($value, $fixed);
foreach($argv as $value) {
echo "Cleaning $value\n";
$content = file_get_contents($value);
$pat = '/(\\\\(?:label|cref|Cref|ref))\\{([^}]+)\\}/';
$fixed = preg_replace_callback($pat, function($match) {
return $match[1] . '{' . trim(str_replace('-', '_', $match[2])) . '}';
}, $content);
file_put_contents($value, $fixed);
}
echo "OK.\n";