]> matita.cs.unibo.it Git - helm.git/commitdiff
camlp5.gramlib does not pull in camlp-streams by default
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 5 Jan 2023 20:31:32 +0000 (21:31 +0100)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 5 Jan 2023 20:31:32 +0000 (21:31 +0100)
matita/components/extlib/dune

index 122907eb7ea05b896e19255963b84da964409c49..c10cd818e1bdea101943c9f309549e0a60ff88b0 100644 (file)
@@ -1,6 +1,6 @@
 (library
  (name helm_extlib)
- (libraries str unix camlp5.gramlib)
+ (libraries str unix camlp-streams camlp5.gramlib) ; camlp-streams should be pulled in by camlp5...
  (modules (:standard \ componentsConf))
  (wrapped false))
 (env