diff options
author | Izorkin <Izorkin@gmail.com> | 2017-11-27 12:44:18 +0300 |
---|---|---|
committer | Jörg Thalheim <Mic92@users.noreply.github.com> | 2017-11-27 09:44:18 +0000 |
commit | 9216f5fc56cb5305bf74b4597f0f06de3c40d412 (patch) | |
tree | b90ecc900db5e75968f03c38ee651c593f2eef5d /pkgs/shells | |
parent | d0f3035e4800141594770ac79994eec58084d5e9 (diff) |
zsh-command-time: init at 2017-05-09 (#32083)
Diffstat (limited to 'pkgs/shells')
-rw-r--r-- | pkgs/shells/zsh-command-time/default.nix | 31 |
1 files changed, 31 insertions, 0 deletions
diff --git a/pkgs/shells/zsh-command-time/default.nix b/pkgs/shells/zsh-command-time/default.nix new file mode 100644 index 0000000000000..453a577440711 --- /dev/null +++ b/pkgs/shells/zsh-command-time/default.nix @@ -0,0 +1,31 @@ +{ stdenv, fetchFromGitHub }: + +# To make use of this plugin, need to add +# programs.zsh.interactiveShellInit = '' +# source ${pkgs.zsh-command-time}/share/zsh-command-time/command-time.plugin.zsh +# ZSH_COMMAND_TIME_MIN_SECONDS=3 +# ZSH_COMMAND_TIME_ECHO=1 +# ''; + +stdenv.mkDerivation rec { + version = "2017-05-09"; + name = "zsh-command-time-${version}"; + + src = fetchFromGitHub { + owner = "popstas"; + repo = "zsh-command-time"; + rev = "2111361cbc88c542c834fbab7802ae5ae8339824"; + sha256 = "0hr9c7196wy9cg7vkmknszr2h446yvg9pqrq0rf3213kz074dhpg"; + }; + + installPhase = '' + install -D $src/command-time.plugin.zsh --target-directory=$out/share/zsh-command-time + ''; + + meta = with stdenv.lib; { + description = "Plugin that output time: xx after long commands"; + homepage = https://github.com/popstas/zsh-command-time; + license = licenses.mit; + platforms = platforms.unix; + }; +} |