diff options
| -rwxr-xr-x | doc/scripts/configure.pl (renamed from configure.pl) | 0 |
1 files changed, 0 insertions, 0 deletions
diff --git a/configure.pl b/doc/scripts/configure.pl index 4859ede74..4859ede74 100755 --- a/configure.pl +++ b/doc/scripts/configure.pl |