[Pkg-haskell-commits] [SCM] Packaging for Agda branch, master, updated. debian/2.3.2-1

[Iain Lane]

The following commit has been merged in the master branch:
commit 9e0ba228deee9b415a6f9027b20f43d8e11361b1
Author: Iain Lane <laney at debian.org>
Date:   Tue Dec 25 13:56:00 2012 +0000

    Add agda-bin package here, as the separate package has been removed

diff --git a/debian/agda-bin.install b/debian/agda-bin.install
new file mode 100644
index 0000000..f7ad685
--- /dev/null
+++ b/debian/agda-bin.install
@@ -0,0 +1 @@
+dist-ghc/build/agda/agda usr/bin
diff --git a/debian/control b/debian/control
index 145b02d..4ede546 100644
--- a/debian/control
+++ b/debian/control
@@ -131,8 +131,8 @@ Architecture: all
 Section: misc
 Depends: ${misc:Depends},
          libghc-agda-dev,
-         agda-mode,
          agda-bin,
+         agda-mode,
          agda-stdlib,
          agda-stdlib-doc
 Description: dependently typed functional programming language
@@ -150,3 +150,27 @@ Description: dependently typed functional programming language
  .
  This is a meta package which provides Agda's emacs mode, executable, standard
  library and its documentation.
+
+Package: agda-bin
+Architecture: any
+Depends: ${shlibs:Depends}, ${haskell:Depends}, ${misc:Depends}
+Recommends: ${haskell:Recommends},
+            libghc-agda-dev (>= 2.3.2),
+            libghc-agda-dev (<< 2.3.2)
+Suggests: ${haskell:Suggests}, agda-mode
+Description: commandline interface to Agda
+ Agda is a dependently typed functional programming language: It has inductive
+ families, which are like Haskell's GADTs, but they can be indexed by values and
+ not just types. It also has parameterised modules, mixfix operators, Unicode
+ characters, and an interactive Emacs interface (the type checker can assist in
+ the development of your code).
+ .
+ Agda is also a proof assistant: It is an interactive system for writing and
+ checking proofs. Agda is based on intuitionistic type theory, a foundational
+ system for constructive mathematics developed by the Swedish logician Per
+ Martin-Löf. It has many similarities with other proof assistants based on
+ dependent types, such as Coq, Epigram and NuPRL.
+ .
+ This package provides a command-line program for type-checking and compiling
+ Agda programs. The program can also generate hyperlinked, highlighted HTML
+ files from Agda sources. 

-- 
Packaging for Agda