[alias] removed some files / options
Showing
- src/plugins/alias/Makefile 0 additions, 76 deletionssrc/plugins/alias/Makefile
- src/plugins/alias/dune 0 additions, 5 deletionssrc/plugins/alias/dune
- src/plugins/alias/dune-project 1 addition, 11 deletionssrc/plugins/alias/dune-project
- src/plugins/alias/dune-workspace 0 additions, 27 deletionssrc/plugins/alias/dune-workspace
- src/plugins/alias/frama-c-alias.opam 0 additions, 38 deletionssrc/plugins/alias/frama-c-alias.opam
- src/plugins/alias/frama-c-alias.opam.template 0 additions, 14 deletionssrc/plugins/alias/frama-c-alias.opam.template
src/plugins/alias/Makefile
deleted
100644 → 0
src/plugins/alias/dune-workspace
deleted
100644 → 0
Please register or sign in to comment