diff options
| author | V3n3RiX <venerix@koprulu.sector> | 2022-11-20 01:01:31 +0000 |
|---|---|---|
| committer | V3n3RiX <venerix@koprulu.sector> | 2022-11-20 01:01:31 +0000 |
| commit | 5d0c0ffd63620a4db788484bd36ab92b76e7891b (patch) | |
| tree | b4204d122504a5c2d3bfdb2cc9f3a5dcf5fe07b2 /dev-ml/ptmap/files | |
| parent | 60945053af0588a6219a4a6867aace9e7b47faeb (diff) | |
gentoo auto-resync : 20:11:2022 - 01:01:31
Diffstat (limited to 'dev-ml/ptmap/files')
| -rw-r--r-- | dev-ml/ptmap/files/ptmap-2.0.5-dune.patch | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/dev-ml/ptmap/files/ptmap-2.0.5-dune.patch b/dev-ml/ptmap/files/ptmap-2.0.5-dune.patch new file mode 100644 index 000000000000..b13122884adb --- /dev/null +++ b/dev-ml/ptmap/files/ptmap-2.0.5-dune.patch @@ -0,0 +1,11 @@ +--- a/dune ++++ b/dune +@@ -1,7 +1,6 @@ + (library + (public_name ptmap) +- (modules ptmap) +- (libraries seq)) ++ (modules ptmap)) + + (test + (name test) |