diff options
Diffstat (limited to 'dev-ml/reason/files/reason-3.12.0-fake-git-version.patch')
| -rw-r--r-- | dev-ml/reason/files/reason-3.12.0-fake-git-version.patch | 13 |
1 files changed, 0 insertions, 13 deletions
diff --git a/dev-ml/reason/files/reason-3.12.0-fake-git-version.patch b/dev-ml/reason/files/reason-3.12.0-fake-git-version.patch deleted file mode 100644 index a00a2e063b84..000000000000 --- a/dev-ml/reason/files/reason-3.12.0-fake-git-version.patch +++ /dev/null @@ -1,13 +0,0 @@ ---- a/src/refmt/dune 2024-10-19 14:08:14.370857664 +0200 -+++ b/src/refmt/dune 2024-10-19 14:09:03.820258355 +0200 -@@ -10,8 +10,8 @@ - (with-stdout-to - %{targets} - (progn -- (bash "echo let version = \\\"$(git rev-parse --verify HEAD)\\\"") -- (bash "echo let short_version = \\\"$(git rev-parse --short HEAD)\\\""))))) -+ (bash "echo let version = \\\"0000000000000000000000000000000000000000\\\"") -+ (bash "echo let short_version = \\\"0000000000000000000000000000000000000000\\\""))))) - - (rule - (with-stdout-to |