diff options
Diffstat (limited to 'dev-ml/reason/files/reason-3.10.0-fake-git-version.patch')
| -rw-r--r-- | dev-ml/reason/files/reason-3.10.0-fake-git-version.patch | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/dev-ml/reason/files/reason-3.10.0-fake-git-version.patch b/dev-ml/reason/files/reason-3.10.0-fake-git-version.patch new file mode 100644 index 000000000000..f4be44e80e2f --- /dev/null +++ b/dev-ml/reason/files/reason-3.10.0-fake-git-version.patch @@ -0,0 +1,10 @@ +--- a/src/refmt/dune ++++ b/src/refmt/dune +@@ -10,5 +10,5 @@ + (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\\\""))))) |